Wyniki wyszukiwania - BazTech

1

Combining Static and Dynamic Contract Checking for Curry

Hanus Michael

Fundamenta Informaticae

|

2020

|

Vol. 173, nr 4

285--314

EN

Static type systems are usually not sufficient to express all requirements on function calls. Hence, contracts with pre- and postconditions can be used to express more complex constraints on operations. Contracts can be checked at run time to ensure that operations are only invoked with reasonable arguments and return intended results. Although such dynamic contract checking provides more reliable program execution, it requires execution time and could lead to program crashes that might be detected with more advanced methods at compile time. To improve this situation for declarative languages, we present an approach to combine static and dynamic contract checking for the functional logic language Curry. Based on a formal model of contract checking for functional logic programming, we propose an automatic method to verify contracts at compile time. If a contract is successfully verified, it can be omitted from dynamic checking. This method decreases execution time without degrading reliable program execution. In the best case, when all contracts are statically verified, it provides trust in the software since crashes due to contract violations cannot occur during program execution.

2

From arithmetic expressions to propositional formulae

Stępień L., Stępień M. R.

Scientific Issues of Jan Długosz University in Częstochowa. Mathematics

|

2016

|

Vol. 21

135--143

EN

In papers [3], [4], [5] Authors presented a new method of solving some kinds of computational tasks in the area of linear algebra by applying SAT-solver as the highly optimized algorithms for solving the problem of propositional satisfiability. On input SAT-solver (cf. [1], [2]) takes a propositional formula in the clause form. In this paper we show in detail how any arithmetical expression can be translated into propositional formula in the CNF form skipping out its traditional form. For this, we define the notion of consistency of arithmetic and boolean valuations.

3

SAT as a Programming Environment for Linear Algebra

Srebrny M., Stępień L.

Fundamenta Informaticae

|

2010

|

Vol. 102, nr 1

115-127

EN

In this paper we pursue the propositional calculus and the SATisfiability solvers as a powerful declarative programming environment that makes it possible to create and run the propositional declarative programs for computational tasks in various areas of mathematics. We report some experimental results on our application of the propositional SATisfiability environment to computing some simple orthogonal matrices and the orders of some orthogonal groups. Some encouraging (and not very encouraging) experiments are reported for the proposed propositional search procedures using off-the-shelf general-purpose SAT solvers. Our new software toolkit SAT4Alg is announced.

4

Wyrażanie kontekstu w przestrzeniach informacji

Bartoszek J., Brzykcy G.

Studia z Automatyki i Informatyki

|

2005

|

T. 30

7--16

PL

W pracy nawiązano do różnych koncepcji definiowania i wyrażania kontekstu wykorzystywanych w systemach informatycznych. Szczególną uwagę zwrócono na te systemy, w których wymiana danych i koordynacja działań agentów są realizowane za pomocą przestrzeni współdzielonych dokumentów XML. Opisano podstawowe pojęcia i mechanizmy związane z takimi przestrzeniami. W pracy zawarto także wstępną propozycję uwzględnienia kontekstu w takich przestrzeniach. W proponowanej koncepcji wykorzystano mechanizmy programowania deklaratywnego.

EN

Various concepts of the context in information systems are presented. A special attention is paid to systems in which data can be exchanged and agent actions can be coordinated via XML document spaces. Main concepts of these document spaces are described. This paper presents a preliminary concept of using context in these spaces. This solution adopts declarative programming mechanisms.

5

Współczesne narzędzia informatyczne wspomagające modelowanie i symulacje procesów dynamicznych

Molenda K., Dąbkowski J.

Inżynieria Rolnicza

|

2002

|

R. 6, nr 6

389--398

PL

Przedstawiono metodologię budowy modeli symulacyjnych znaną jako Dynamika Systemów, opracowaną w latach sześćdziesiątych w Sloan School of Management, Massachusset Institute of Technology. Zaprezentowano współczesne narzędzia informatyczne implementujące tę metodę, wskazując możliwości ich wykorzystania w pracach badawczych oraz dydaktyce.

EN

Paper presented the methodology of developing simulation models, known as the systems Dynamics elaborated in the sixties at Sloan School of Management, Massachus- sets Institute of Technology. There were also described the recent information technology instruments implementing these methods and indicating the possibilities of their application both, in the research works and teaching.

6

Declarativity in modelling and problem solving

Niederliński A.

Control and Cybernetics

|

2000

|

Vol. 29, no 1

325-339

EN

The paper discusses a new trend in the modelling software for combinatorial and mixed combinatorial-continuous decision problems. The trend, aiming at solving those problems by the simple activity of properly describing them, is best exemplified by a constantly inereasing spectrum of Constraint Logic Programming (CLP) languages. The first such language was Prolog. After a short historical survey concentrating mainly on Prolog, main characteristics of a modern, commercially successful CLP language - CHIP - are presented, discussed and illustrated. The CLP approach to problem solving is compared with traditional Operation Research approaches.