Operational and goal-independent denotational semantics for Prolog with cut

In this paper we propose an operational and a denotational semantics for Prolog. We deal with the control rules of Prolog and the cut operator. Our denotational semantics provides a goal-independent semantics. This means that the behaviour of a goal in a program is defined as the evaluation of the goal in the denotation (semantics) of the program. We show how our denotational semantics can be specialised into a computed answer semantics and into a call pattern semantics. Our work provides a basis for a precise abstract interpretation of Prolog programs.     

Transfinite Semantics in the Form of Greatest Fixpoint

Transfinite semantics is a semantics according to which program executions can continue working after an infinite number of steps. Such a view of programs can be useful in the theory of program transformations.So far, transfinite semantics have been succesfully defined for iterative loops. This paper provides an exhaustive definition for semantics that enable also infinitely deep recursion.The definition is actually a parametric schema that defines a family of different transfinite semantics. As standard semantics also match the same schema, our framework describes both standard and transfinite semantics in a uniform way.All semantics are expressed as greatest fixpoints of monotone operators on some complete lattices. It turns out that, for transfinite semantics, the corresponding lattice operators are cocontinuous. According to Kleene’s theorem, this shows that transfinite semantics can be expressed as a limit of iteration which is not transfinite.     

Mechanizing some advanced refinement concepts

We describe how the HOL theorem prover can be used to check and apply rules of program refinement. The rules are formulated in the refinement calculus, which is a theory of correctness preserving program transformations. We embed a general command notation with a predicate transformer semantics in the logic of the HOL system. Using this embedding, we express and prove rules for data refinement and superposition refinement of initialized loops. Applications of these proof rules to actual program refinements are checked using the HOL system, with the HOL system generating these conditions. We also indicate how the HOL system is used to prove the verification conditions. Thus, the HOL system can provide a complete mechanized environment for proving program refinements.     

Linear Approximation of Execution-Time Constraints

This paper defines an algorithm for predicting worst-case and best-case execution times, and determining execution-time constraints of control-flow paths through real-time programs using their partial correctness semantics. The algorithm produces a linear approximation of path traversal conditions, worst-case and best-case execution times and strongest postconditions for timed paths in abstract real-time programs. Also shown are techniques for determining the set of control-flow paths with decidable worst-case and best-case execution times. The approach is based on a weakest liberal precondition semantics and relies on supremum and infimum calculations similar to standard computations from linear programming and Presburger arithmetic. The methodology is applicable to any executable language with a predicate transformer semantics and hence provides a verification basis for both high-level language and assembly code execution-time analysis.     

Uniform Closures: Order-Theoretically Reconstructing Logic Program Semantics and Abstract Domain Refinements

The notion of uniform closure operator is introduced, and it is shown how this concept surfaces in two different areas of application of abstract interpretation, notably in semantics design for logic programs and in the theory of abstract domain refinements. In logic programming, uniform closures permit generalization, from an order-theoretic perspective, of the standard hierarchy of declarative semantics. In particular, we show how to reconstruct the model-theoretic characterization of the well-known s-semantics using pure order-theoretic concepts only. As far as the systematic refinement operators on abstract domains are concerned, we show that uniform closures capture precisely the property of a refinement of being invertible, namely of admitting a related operator that simplifies as much as possible a given abstract domain of input for that refinement. Exploiting the same argument used to reconstruct the s-semantics of logic programming, we yield a precise relationship between refinements and their inverse operators: we demonstrate that they form an adjunction with respect to a conveniently modified complete order among abstract domains.     

基于抽象解释的Prolog程序验证技术研究

作为一种通用的语义近似理论,抽象解释已广泛应用于各类程序的形式化验证中.现有基于抽象解释的逻辑程序验证技术未涉及与程序点相关联的程序性质的验证,设计能够描述此类性质的逻辑程序具体语义和抽象语义是构造相应验证工具的关键.本文给出了一种基于抽象解释的Prolog程序验证方法,该方法采用了具有路径信息的Prolog语义及其抽象作为语义基础,因而可用于验证与程序点相关联的程序特性.本文例子表明了该验证方法的有效性.     

Formal verification of Ada programs

The Penelope verification editor and its formal basis are described. Penelope is a prototype system for the interactive development and verification of programs that are written in a rich subset of sequential Ada. Because it generates verification conditions incrementally, Penelope can be used to develop a program and its correctness proof in concert. If an already-verified program is modified, one can attempt to prove the modified version by replaying and modifying the original sequence of proof steps. Verification conditions are generated by predicate transformers whose logical soundness can be proven by establishing a precise formal connection between predicate transformation and denotational definitions in the style of continuation semantics. Penelope's specification language, Larch/Ada, belongs to the family of Larch interface languages. It scales up properly, in the sense that one can demonstrate the soundness of decomposing an implementation hierarchically and reasoning locally about the implementation of each node in the hierarchy     

Frame rule for mutually recursive procedures manipulating pointers

Using a predicate transformer semantics of programs, we introduce statements for heap operations and separation logic operators for specifying programs that manipulate pointers. We prove a powerful Hoare total correctness rule for mutually recursive procedures manipulating pointers. The rule combines earlier proof rules for (mutually) recursive procedures with the frame rule for pointer programs. The theory, including the proofs, is implemented in the theorem prover PVS. In this implementation program variables and addresses can store values of almost any type of the theorem prover.     

A security flow control algorithm and its denotational semantics correctness proof

We derive a security flow control algorithm for message-based, modular systems and prove the algorithm correct. The development is noteworthy because it is completely rigorous: the flow control algorithm is derived as an abstract interpretation of the denotational semantics of the programming language for the modular system, and the correctness proof is a proof by logical relations of the congruence between the denotational semantics and its abstract interpretation. Effectiveness is also addressed: we give conditions under which an abstract interpretation can be computed as a traditional iterative data flow analysis, and we prove that our security flow control algorithm satisfies the conditions. We also show that symbolic expressions (that is, data flow values that contain unknowns) can be used in a convergent, iterative analysis. An important consequence of the latter result is that the security flow control algorithm can analyse individual modules in a system for well formedness and later can link the analyses to obtain an analysis of the entire system.     

Semantic theories of programs with nested interrupts

In the design of dependable software for embedded and real-time operating systems, time analysis is a crucial but extremely difficult issue, the challenge of which is exacerbated due to the randomness and nondeterminism of interrupt handling behaviors. Thus research into a theory that integrates interrupt behaviors and time analysis seems to be important and challenging. In this paper, we present a programming language to describe programs with interrupts that is comprised of two essential parts: main program and interrupt handling programs. We also explore a timed operational semantics and a denotational semantics to specify the meanings of our language. Furthermore, a strategy of deriving denotational semantics from the timed operational semantics is provided to demonstrate the soundness of our operational semantics by showing the consistency between the derived denotational semantics and the original denotational semantics.     

Data refinement of mixed specifications

Using predicate transformers as a basis, we give semantics and refinement rules for mixed specifications that allow UNITY style specifications to be written as a combination of abstract program and temporal properties. From the point of view of the programmer, mixed specifications may be considered a generalization of the UNITY specification notation to allow safety properties to be specified by abstract programs in addition to temporal properties. Alternatively, mixed specifications may be viewed as a generalization of the UNITY programming notation to allow arbitrary safety and progress properties in a generalized ‘always section’. The UNITY substitution axiom is handled in a novel way by replacing it with a refinement rule. The predicate transformers foundation allows known techniques for algorithmic and data-refinement for weakest precondition based programming to be applied to both safety and progress properties. In this paper, we define the predicate transformer based specifications, specialize the refinement techniques to them, demonstrate soundness, and illustrate the approach with a substantial example. Received: 1 April 1996 / 6 March 1997     

From algebraic semantics to denotational semantics for Verilog

This paper considers how the algebraic semantics for Verilog relates with its denotational semantics. Our approach is to derive the denotational semantics from the algebraic semantics. We first present the algebraic laws for Verilog. Every program can be expressed as a guarded choice that can model the execution of a program. In order to investigate the parallel expansion laws, a sequence is introduced, indicating which instantaneous action is due to which exact parallel component. A head normal form is defined for each program by using a locality sequence. We provide a strategy for deriving the denotational semantics based on head normal form. Using this strategy, the denotational semantics for every program can be calculated. Program equivalence can also be explored by using the derived denotational semantics. A short version of this paper appeared in Proc. ICECCS 2006: 11th IEEE International Conference on Engineering of Complex Computer Systems [48]. This work is partially supported by the National Basic Research Program of China (No. 2005CB321904), the National High Technology Research and Development Program of China (No. 2007AA010302) and the National Natural Science Foundation of China (No. 90718004). Jonathan Bowen is a visiting professor at King’s College London and an emeritus professor at London South Bank University.     

A residualizing semantics for the partial evaluation of functional logic programs

Recent proposals for multi-paradigm declarative programming combine the most important features of functional, logic and concurrent programming into a single framework. The operational semantics of these languages is usually based on a combination of narrowing and residuation. In this paper, we introduce a non-standard, residualizing semantics for multi-paradigm declarative programs and prove its equivalence with a standard operational semantics. Our residualizing semantics is particularly relevant within the area of program transformation where it is useful, e.g., to perform computations during partial evaluation. Thus, the proof of equivalence is a crucial result to demonstrate the correctness of (existing) partial evaluation schemes.     

命令的指称语义在谓词域上的一种表示

文中讨论了谓词转换器和状态转换器之间的对应关系,将谓词转换器作为命令的指称,刻画了IMP语言命令的指称语义,并证明与状态转换器形式的指称语义是等价的.     

Semantics of plan revision in intelligent agents

In this paper, we give an operational and denotational semantics for a meta-language of the 3APL agent programming language. With this meta-language, various 3APL interpreters can be programmed. We prove equivalence of the operational and denotational semantics. Furthermore, we give an operational semantics for object-level 3APL. Using this semantics, we relate the 3APL meta-language to object-level 3APL by providing a specific interpreter, the semantics of which will prove to be equivalent to object-level 3APL.     

Unification of Four Versions of Program Semantics

Computing Science is a new subject, and we have not yet achieved the unification of theories that should support a proper understanding of its structure. CAR Hoare and He Jifeng, 1998. In this paper we use Priestley duality and Jónsson/Tarski duality to translate between four versions of program semantics: the relational model, predicate transformer semantics, information systems, and powerdomains. Our point of entry is the relational model, a kind of Kripke semantics, in which programs are thought of as input-output relations over a structured state space. Specifically, we present the state space as a certain kind of Priestley space, and programs as certain structure-preserving relations over such a space. We then derive, in circular fashion, a predicate transformer semantics from the relational model, an information system from the predicate transformer semantics, a powerdomain from the information system, and the original relational model back again from the powerdomain. The information system is also shown to be related to Hoare logic. To clarify the intuition behind this approach we present a case study, which is a ‘Priestley version’ of the so-called universal domain due to Plotkin, and we explicate various ideas about properties of programs and predicates in terms of this case study. Received April 1997 / Accepted in revised form February 1998     

Predicate transformers as power operations

In predicate transformer semantics, a program is represented as a mapping from predicates to predicates. In relational semantics, a program is represented as an (input-output) binary relation over some state space. We show how each of these approaches can be obtained from the other by using thepower construction.     

A non-standard semantics for program slicing and dependence analysis

We introduce a new non-strict semantics for a simple while language. We demonstrate that this semantics allows us to give a denotational definition of variable dependence and neededness, which is consistent with program slicing. Unlike other semantics used in variable dependence, our semantics is substitutive. We prove that our semantics is preserved by traditional slicing algorithms.     

Magic-sets for localised analysis of Java bytecode

Static analyses based on denotational semantics can naturally model functional behaviours of the code in a compositional and completely context and flow sensitive way. But they only model the functional i.e., input/output behaviour of a program P, not enough if one needs P’s internal behaviours i.e., from the input to some internal program points. This is, however, a frequent requirement for a useful static analysis. In this paper, we overcome this limitation, for the case of mono-threaded Java bytecode, with a technique used up to now for logic programs only. Namely, we define a program transformation that adds new magic blocks of code to the program P, whose functional behaviours are the internal behaviours of P. We prove the transformation correct w.r.t. an operational semantics and define an equivalent denotational semantics, devised for abstract interpretation, whose denotations for the magic blocks are hence the internal behaviours of P. We implement our transformation and instantiate it with abstract domains modelling sharing of two variables, non-cyclicity of variables, nullness of variables, class initialisation information and size of the values bound to program variables. We get a static analyser for full mono-threaded Java bytecode that is faster and scales better than another operational pair-sharing analyser. It has the same speed but is more precise than a constraint-based nullness analyser. It makes a polyhedral size analysis of Java bytecode scale up to 1300 methods in a couple of minutes and a zone-based size analysis scale to still larger applications.     

Towards a semantics-based information theory

We develop a formal framework to give computer programs an abstract interpretation as information transformers. Then the quantitative relation between input and output information is investigated. Our theory is based oninformation domains, a refinement of the classical domains used in denotational semantics, and on the theory of abstract interpretation of functional languages.