Program development can be made amenable to formal methods by using a logical framework. A logic specification, whose operational semantics is based on proof theory, provides an abstract and “implementation independ...
详细信息
ISBN:
(纸本)0897914724
Program development can be made amenable to formal methods by using a logical framework. A logic specification, whose operational semantics is based on proof theory, provides an abstract and “implementation independent” definition of the problem, the data domains and the associated *** many of the current efforts in this area that use resolution, our approach is based on natural deduction, more specifically, sequent calculus. Following the methodology proposed by Manna and Waldinger, we propose the synthesis tableau technique by which we construct a proof for the well formed formula representing the specification. The desired program is obtained as a side effect of the proof process.
A general definition of constraint systems utilizing Gentzen-style sequents is given. Constraint systems can be regarded as enriching the propositional Scott information systems with minimal first-order structure: the...
详细信息
ISBN:
(纸本)0818627352
A general definition of constraint systems utilizing Gentzen-style sequents is given. Constraint systems can be regarded as enriching the propositional Scott information systems with minimal first-order structure: the notion of variables, existential quantification, and substitution. Approximate maps that are generic in all but finitely many variables are taken as morphisms. It is shown that the resulting structure forms a category (called ConstSys). Furthermore, the structure of Scott information systems lifts smoothly to the first-order setting. In particular, it is shown that the category is Cartesian-closed, and other usual functors over Scott information systems (lifting, sums, Smyth power-domain) are also definable and recursive domain equations involving these functors can be solved.
In this paper an effective decomposition algorithm for mapping of logic functions onto FPGAs is proposed. The algorithm exploits our symbolic decomposition concept to find FPGA based implementation with a minimal numb...
详细信息
ISBN:
(纸本)0818628456
In this paper an effective decomposition algorithm for mapping of logic functions onto FPGAs is proposed. The algorithm exploits our symbolic decomposition concept to find FPGA based implementation with a minimal number of CLBs. Experimental results of the presented method are provided and compared to other similar tools.
Finite-state programs over real-numbered time in a guarded-command language with real-valued clocks are described. Model checking answers the question of which states of a real-time program satisfy a branching-time sp...
详细信息
ISBN:
(纸本)0818627352
Finite-state programs over real-numbered time in a guarded-command language with real-valued clocks are described. Model checking answers the question of which states of a real-time program satisfy a branching-time specification. An algorithm that computes this set of states symbolically as a fixpoint of a functional on state predicates, without constructing the state space, is given.
A new formal embodiment of J.-Y. Girard's (1989) geometry of interaction program is given. The geometry of interaction interpretation considered is defined, and the computational interpretation is sketched in term...
详细信息
ISBN:
(纸本)0818627352
A new formal embodiment of J.-Y. Girard's (1989) geometry of interaction program is given. The geometry of interaction interpretation considered is defined, and the computational interpretation is sketched in terms of dataflow nets. Some examples that illustrate the key ideas underlying the interpretation are given. The results, which include the semantic analogue of cut-elimination, stated in terms of a finite convergence property, are outlined.
We are investigating the claim that object-oriented analysis (OOA) requirements models can be changed, reused, and integrated more easily than other kinds of requirements models. In this paper, we describe one part of...
详细信息
ISBN:
(纸本)0897915046
We are investigating the claim that object-oriented analysis (OOA) requirements models can be changed, reused, and integrated more easily than other kinds of requirements models. In this paper, we describe one part of that investigation: an experiment involving an OOA method in which the requirements for an automated teller machine (ATM) system are changed and the effects on the model are assessed.
The catch/throw mechanism, a programming construct for nonlocal exit, plays an important role when programmers handle exceptional situations. A constructive formalization that captures the mechanism in the proofs-as-p...
详细信息
ISBN:
(纸本)0818627352
The catch/throw mechanism, a programming construct for nonlocal exit, plays an important role when programmers handle exceptional situations. A constructive formalization that captures the mechanism in the proofs-as-programs notion is given. A modified version of LJ equipped with inference rules corresponding to the operations of catch and throw is introduced. Then it is shown that one can actually extract programs that make use of the catch/throw mechanism from proofs under a certain realizability interpretation. Although the catch/throw mechanism provides only a restricted access to the current continuation, the formulation remains constructive.
Trace assertion specification methods constrain behaviour at the interface of a module by identifying legal sequences of calls to the module's access programs. The legality of extending a trace by a call is specif...
详细信息
Trace assertion specification methods constrain behaviour at the interface of a module by identifying legal sequences of calls to the module's access programs. The legality of extending a trace by a call is specified by assertions that express properties that the trace and call must satisfy. Trace specifications can often be simplified by formulating assertions about representative normal (or canonical) form traces, but this approach is only useful when convenient forms can be found. This paper: 1) introduces a new trace assertion method, called the Property Vector (PV) method, 2) demonstrates the method by specifying a multiset iterator module previously identified as difficult to specify [Lam90], 3) compares the PV method to other methods. The main new feature of the PV method is the use of a vector of property variables that explicitly represent relevant properties of a trace that influence a module's future behaviour. It is possible to obtain a simple trace assertion specification for a module even though convenient (legal) normal/canonical form traces are not apparent. Normal/canonical form trace assertion methods are special cases of the PV method where the only relevant property of a trace is its equivalent normal/canonical form.
Recently, considerable interest arose in integrating object-oriented and logic programming. In this paper, we describe an object-oriented logic programming language and discuss its extension by exploring its roles and...
详细信息
ISBN:
(纸本)0818628308
Recently, considerable interest arose in integrating object-oriented and logic programming. In this paper, we describe an object-oriented logic programming language and discuss its extension by exploring its roles and representations to artificial intelligence frame system and production system. In particular, we describe how to add derived slots into classes and to represent production rules in an object-oriented production system, forming a framework of knowledge-based system with multiple paradigms.
This paper provides a link between the formulation of static program analyses using the framework of abstract interpretation (popular for functional languages) and using the more classical framework of data flow analy...
详细信息
ISBN:
(纸本)0897914813
This paper provides a link between the formulation of static program analyses using the framework of abstract interpretation (popular for functional languages) and using the more classical framework of data flow analysis (popular for imperative languages). In particular we show how the classical notions of fastness, rapidity and k-boundedness carry over to the abstract interpretation framework and how this may be used to bound the number of times a functional should be unfolded in order to yield the fixed point. This is supplemented with a number of results on how to calculate the bounds for iterative forms (as for tail recursion), for linear forms (as for one nested recursive call), and for primitive recursive forms. In some cases this improves the `worst case' results of [9], but more importantly it gives much better `average case' results.
暂无评论