Stack method in program semantics

In this paper,we describe firstly a formal concept of stack and introduce some operational rules on it.Then we extend the denotational semantics to“the denotational semantics with stacks”,by which we makea formal semantics for a real PASCAL(subset)which can run on a computer.By an example of programwith procedures it will be seen that our method can be used to describe the basic principles of compiling.Finally,we have succeeded in building a formal semantics model of a PROLOG(subset).     

Circular expressions: elimination of static environments

Consider the connection between denotational semantics for a language with goto statements and flow diagrams for programs in such a language. The main point of interest is that the denotational semantics uses a recursively defined environment to give the meaning of labels, while a flow diagram merely has a jump to the appropriate program point. A simple reduction called “indirection elimination” strips away the environment from the denotational semantics and extracts an expression with cycles that is very close to the flow diagram of a program. The same idea applies to associating bodies with recursive procedures, or to any construct whose semantics is not wedded to the syntax. In addition to being a useful data structure and conceptual device, expressions with cycles are well defined mathematical objects—their semantics can be given by unfolding them into infinite structures that have been well studied. The practicality of the elimination of environments has been tested by constructing a trial implementation, which serves as the front end of a semantics directed compiler generator. The implementation takes a denotational semantics of a language and constructs a “black box” that maps programs in the language into an intermediate representation. The intermediate representation is a circular expression.     

A Provably Correct Translation of the λ-Calculus into a Mathematical Model of C++

We introduce a translation of the simply typed λ-calculus into C++, and give a mathematical proof of the correctness of this translation. For this purpose we develop a suitable fragment of C++ together with a denotational semantics. We introduce a formal translation of the λ-calculus into this fragment, and show that this translation is correct with respect to the denotational semantics. We show as well a completeness result, namely that by translating λ-terms we obtain essentially all C++ terms in this fragment. We introduce a mathematical model for the evaluation of programs of this fragment, and show that the evaluation computes the correct result with respect to this semantics.     

Operational domain theory and topology of sequential programming languages

A number of authors have exported domain-theoretic techniques from denotational semantics to the operational study of contextual equivalence and order. We further develop this, and, moreover, we additionally export topological techniques. In particular, we work with an operational notion of compact set and show that total programs with values on certain types are uniformly continuous on compact sets of total elements. We apply this and other conclusions to prove the correctness of non-trivial programs that manipulate infinite data. What is interesting is that the development applies to sequential programming languages, in addition to languages with parallel features.     

An operational formal definition of PROLOG: a specification method and its application

We present in this paper a logic programming specification language and its application to the formal specification of PROLOG dialects (Marseille-Edinburgh like dialect or parallel logic programs). In particular it is used in the standardization work of PROLOG. The specification language is based on normal clauses (definite clauses with possibly negative literals in the body) whose semantics is the set of the (generalized) proof-trees. We restrict the specification language to stratified programs and ground proof-trees such that its semantics fits with most of the usual known semantics in logic programming. The specification language is fully declarative in the sense that it is written in a pure logical stule. It is relatively easy to deduce an executable specification from a specification written in such a language. Part of the specification are the associated comments and a methodology has been developed to write these. Without the comments a formal specification cannot be understood; they are partly formal and serve only to help to understand the axioms. They are a natural language form of formal statements relative to the correctness and the completeness of the axioms with regards to some intended meaning. We show in this paper how this specification language can be used to specify dialects of PROLOG. The presented example is just a sample of PROLOG but fully developed here. The specification language has already been used for real dialects as PARLOG and standard PROLOG. This specification method is also interesting because it illustrates the power of logic programming to make specifications. It seems to us that logic programming is generally considered as “impure” executable specification. Our purpose is to show that logic programming may also be used as a perhaps low level but full specification language.     

Algebraic approach to linking the semantics of web services

Web services have become more and more important in these years, and BPEL4WS (BPEL) is a de facto standard for the web service composition and orchestration. It contains several distinct features, including the scope-based compensation and fault handling mechanism. We have considered the operational semantics and denotational semantics for BPEL, where a set of algebraic laws can be achieved via these two models, respectively. In this paper, we consider the inverse work, deriving the operational semantics and denotational semantics from algebraic semantics for BPEL. In our model, we introduce four types of typical programs, by which every program can be expressed as the summation of these four types. Based on the algebraic semantics, the strategy for deriving the operational semantics is provided and a transition system is derived by strict proof. This can be considered as the soundness exploration for the operational semantics based on the algebraic semantics. Further, the equivalence between the derivation strategy and the derived transition system is explored, which can be considered as the completeness of the operational semantics. Finally, the derivation of the denotational semantics from algebraic semantics is explored, which can support to reason about more program properties easily.     

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.     

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.     

The occur-check problem revisited

A method is presented for executing PROLOG programs which avoids almost all unnecessary occur-checks. The method is based on a dynamic classification of the context in which logical variables occur. No static global analysis of the PROLOG program is required to detect the places where an occur-check has to be made. The presented method has also an important side benefit. It considerably cuts down on the number of memory references during the execution of PROLOG programs. Furthermore, in most cases it avoids “trailing” and “untrailing” of unbound variables altogether. Due to this fact the employed method actually speeds up PROLOG execution. The method is discussed in terms of an actual implementation based on the Warren abstract PROLOG instruction set. However, the method should be applicable to other implementation models as well. No assumptions are made with respect to particular hardware.     

Non-Standard Semantics for Program Slicing

In this paper we generalize the notion of compositional semantics to cope with transfinite reductions of a transition system. Standard denotational and predicate transformer semantics, even though compositional, provide inadequate models for some known program manipulation techniques. We are interested in the systematic design of extended compositional semantics, observing possible transfinite computations, i.e. computations that may occur after a given number of infinite loops. This generalization is necessary to deal with program manipulation techniques modifying the termination status of programs, such as program slicing. We include the transfinite generalization of semantics in the hierarchy developed in 1997 by P. Cousot, where semantics at different levels of abstraction are related with each other by abstract interpretation. We prove that a specular hierarchy of non-standard semantics modeling transfinite computations of programs can be specifiedin such a way that the standard hierarchy can be derived by abstract interpretation. We prove that non-standard transfinite denotational and predicate transformer semantics can be both systematically derived as solutions of simple abstract domain equations involving the basic operation of reduced power of abstract domains. This allows us to prove the optimality of these semantics, i.e. they are the most abstract semantics in the hierarchy which are compositional and observe respectively the terminating and initial states of transfinite computations, providing an adequate mathematical model for program manipulation.     

Some applications of topology to program semantics

The relationship between programs and the set of partial correctness assertions that they satisfy, constitutes a Galois connection. The topology resulting from this Galois connection is closely related to the Lindenbaum baum topology for the language in which these partial correctness assertions are stated. This relationship provides us with a tool for understanding the incompleteness of Hoare Logics and for answering certain natural questions about the connection between the relational semantics and the partial correctness assertion semantics for programs, especially in connection with the question of modularity of programs. Two questions to which we shall find topological answers in this paper are “When is a language expressive for a program?”, and “When can we have rules of inference which are adequate to infer the properties of the complex program ±#β from those of its components ±,β?” We also obtain a natural answer to the question “What can the set{(A, B)|{A}±{B} is true) look like for arbitraryα?”.     

Relating confluence,innermost-confluence and outermost-confluence properties of term rewriting systems

Innermost-confluence is important in giving call-by-value and denotational semantics and outermost-confluence is important in giving call-by-need and lazy semantics of programs. In this paper, we give a few sets of sufficient conditions under which the properties of confluence, innermost-confluence and outermost-confluence coincide. Confluence and innermost-confluence coincide for weakly innermost normalizing overlay systems and confluence and outermost-confluence coincide for outermost normalizing left-linear overlay systems. In general, every weakly innermost (outermost) normalizingconfluent system isinnermost (outermost) confluent but the converse is not true.     

Bundle event structures: A revised cpo approach

Bundle event structures equipped with a partial order ? have been used to give a true concurrency denotational semantics for LOTOS. This model has also been extended by time and stochastic information. Unfortunately it fails to yield a complete partial order (cpo) as we illustrate by an example.We propose a subset of all bundle event structures such that it forms a cpo. This subset is closed under the usual operators on bundle event structures. And as a consequence these operators are continuous. Therefore, this subset can be used to give a denotational semantics of LOTOS.     

LCF considered as a programming language

The paper studies connections between denotational and operational semantics for a simple programming language based on LCF. It begins with the connection between the behaviour of a program and its denotation. It turns out that a program denotes ⊥ in any of several possible semantics if it does not terminate. From this it follows that if two terms have the same denotation in one of these semantics, they have the same behaviour in all contexts. The converse fails for all the semantics. If, however, the language is extended to allow certain parallel facilities behavioural equivalence does coincide with denotational equivalence in one of the semantics considered, which may therefore be called “fully abstract”. Next a connection is given which actually determines the semantics up to isomorphism from the behaviour alone. Conversely, by allowing further parallel facilities, every r.e. element of the fully abstract semantics becomes definable, thus characterising the programming language, up to interdefinability, from the set of r.e. elements of the domains of the semantics.     

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.     

Sequential algorithms on concrete data structures

We provide a sequential denotational semantics for sequential programming languages, based on a new notion of sequential algorithm on the Kahn-Plotkin concrete data structures. Intuitively an algorithm may be seen either as a concrete object—a “program” in a simple output-driven language — or as an abstract object — the pair of a sequential function and of a computation strategy for it. The concrete and abstract presentations are equivalent, as shown by a representation theorem. The algorithms form a cartesian closed category with straightforward solutions to recursive domain equations. Hence they may replace functions in the denotational semantics of any sequential language. An applicative programming language based on sequential algorithms is presented in a companion paper.     

A reactive extension of the OpenMusic visual programming language

Objectives: OpenMusic (OM) is a domain-specific visual programming language designed for computer-aided music composition. This language based on Common Lisp allows composers to develop functional processes generating or transforming musical data, and to execute them locally by demand-driven evaluations. As most historical computer-aided composition environments, OM relies on a transformational declarative paradigm, which is hard to conciliate with reactive data-flow (an evaluation scheme more adequate to the development of interactive systems). We propose to link these two evaluation paradigms in the same and consistent visual programming framework.Methods: We establish a denotational semantics of the visual language, which gives account for its demand-driven evaluation mechanism and the incremental construction of programs. We then extend this semantics to enable reactive computations in the functional graphs.Results: The resulting language merges data-driven executions with the existing demand-driven mechanism. A conservative implementation is proposed.Conclusions: We show that the incremental construction of programs and their data-driven and demand-driven evaluations can be smoothly integrated in the visual programming workflow. This integration allows for the propagation of changes in the programs, and the evaluation of graphically designed functional expressions as a response to external events, a first step in bridging the gap between computer-assisted composition environments and real-time musical systems.     

Comparative semantics for flow of control in logic programming without logic

We study semantic issues concerning control flow notions in logic programming languages by exploring a two-stage approach. The first considers solely uninterpreted (or schematic) elementary actions, rather than operations such as unification, substitution generation, or refutation. Accordingly, logic is absent at this first stage. We provide a comparative survey of the semantics of a variety of control flow notions in (uninterpreted) logic programming languages including notions such as don't know versus don't care nondeterminism, the cut operator, and/or parallel logic programming, and the commit operator. In all cases considered, we develop operational and denotational models, and prove their equivalence. A central tool both in the definitions and in the equivalence proofs is Banach's theorem on (the uniqueness of) fixed points of contracting functions on complete metric spaces. The second stage of the approach proceeds by interpreting the elementary actions, first as arbitrary state transformations, and next by suitably instantiating the sets of states and of state transformations (and by articulating the way in which a logic program determines a set of recursive procedure declarations). The paper concentrates on the first stage. For the second stage, only a few hints are included. Furthermore, references to papers which supply details for the languages PROLOG and CONCURRENT PROLOG are provided.