An axiomatic definition of the programming language PASCAL

Summary The axiomatic definition method proposed in reference [5] is extended and applied to define the meaning of the programming language PASCAL [1]. The whole language is covered with the exception of real arithmetic and go to statements.     

A complete axiomatic semantics of spawning

Summary In modern imperative languages there are two commonly occurring ways to activate concurrently running tasks,splitting (cobegin...coend) andspawning. The programming language Ada makes use of both forms of task activation. We present a formal system for verifying partial correctness specifications of Ada tasks activated by spawning. The system is based upon a view of tasks as histories of events. We show how the mindset of splitting may be applicable when developing a formal system for reasoning about spawning. The resultant proof system is compositional, and a robust extension of partial correctness proof systems for sequential constructs. A transition model is given for spawning, and the proof system is proven complete in the sense of Cook [10] relative to this model, under certain reasonable assumptions. The specific proof rules given apply to a subset of Ada without real-time and distributed termination. Our approach to task verification applies to other imperative languages besides Ada, and the essential parts of our methodology are applicable to other formal systems besides those based on partial correctness reasoning. Sigurd Meldal is professor of informatics at the University of Bergen. He is interested in techniques and tools based on formal methods for development of concurrent software. His current foci are the investigation of algebraic approaches to nondeterminism, and the participation in the design of a concurrent specification, prototyping and implementation language. The latter supplements formal proof with support for run time control of consistency between concurrent systems as specified and as implemented. Meldal received his cand. real. (1982) and dr. scient. (1986) degrees in informatics from the University of Oslo.This research was supported by a grant from the Norwegian Research Council for Science and the Humanities, by the Defense Advanced Research Projects Agency/Information Systems Technology Office under the office of Naval Research contract N00014-90-J1232, by the Air Force Office of Scientific Research under Grant AFOSR83-0255 and by a Fulbright Scholarship from the US Educational Foundation in Norway     

Two-level grammar as an implementable metalanguage for axiomatic semantics

Two-level grammars can define the syntax and the operational semantics of programming languages and these definitions are directly executable by interpretation. In this paper it is shown that axiomatic semantics can also be defined using a two-level grammar with the result being a partially automatic program verification system accomplished within the framework of a language definition. These results imply that a programming language can be defined operationally and axiomatically together in complementary definitions as advocated by Hoare and Lauer. Because two-level grammars are executable, these complementary definitions accomplish a system for interpreting and verifying programs.     

C-programs verification based on mixed axiomatic semantics

The mixed axiomatic semantics of the C-kernel language is described. This language is the kernel of a representative subset which is called C-light. Such semantics makes possible for the verification conditions to be simplified in many cases. The semantics is the basis of the verification conditions generator for C-kernel programs. An example illustrating the application of the inference rules of the semantics is considered.     

An intermediate language to define dynamic semantics

An instruction set is given for an abstract machine which uses a pushdown stack as its principal memory. The proposed instructions serve the similar purposes of (1) defining the dynamic semantics of programming languages by describing the operations of programs on the abstract machine and (2) describing an intermediate language to be used in compiling programming languages into machine language. It is shown how the intermediate language can be used in the translation of the programming languages ADA, FORTRAN and PASCAL into IBM 360 assembly language and advantages over other intermediate languages such as three-address code and P-code.     

Correctness of the compiling process based on axiomatic semantics

Summary A language that includes computed gotos and parameterized procedures is defined and its semantics are given axiomatically. A number of program transformations are described and proved correct. Taken collectively and applied repeatedly these transformations compile the full language into a low level subset.     

Computability concepts for programming language semantics

This paper is about mathematical problems in programming language semantics and their influence on recursive function theory. We define a notion of computability on continuous higher types (for all types) and show its equivalence to effective operators. This resuit shows that our computable operators can model mathematically (i.e. extensionally) everything that can be done in an operational semantics. These new recursion theoretic concepts which are appropriate to semantics also allow us to construct Scott models for the λ-calculus which contain all and only computably elements. Depending on the choice of the initial cpo, our general theory yields a theory for either strictly determinate or else arbitrary non-deterministic objects (parallelism). The formal theory is developed in Part II of this paper. Part I gives motivation and comparison with related work.     

The axiomatic semantics of programs based on Hoare's logic

Summary This paper is about the Floyd-Hoare Principle which says that the semantics of a programming language can be formally specified by axioms and rules of inference for proving the correctness of programs written in the language. We study the simple language WP of while-programs and Hoare's system for partial correctness and we calculate the relational semantics of WP as this is determined by Hoare's logic. This calculation is possible by using relational semantics to build a completeness theorem for the logic. The resulting semantics AX we call the axiomatic relational semantics for WP. This AX is not the conventional semantics for WP: it need not be effectively computable or deterministic, for example. A large number of elegant properties of AX are proved and the Floyd-Hoare Principle is reconsidered.     

An operational semantics for Icon: Implementation of a procedural goal-directed language

The generation of compiled code for expressions in programming languages such as Icon that support goal-directed evaluation in addition to traditional control structures presents more of a challenge than generating code for traditional imperative programming languages. This paper describes a code-generation technique for translating Icon programs into a traditional high-level language. Translations into both Pascal and C are discussed. However, any language that provides function parameters and recursion is sufficient. The technique described here has been used in the implementation of an optimizing compiler for Icon.     

A Formal Semantics for DAI Language NUML

Traditional AI systems are brittle in the sense that they fail miserably when presented with problems even sliphtly outside of their limited range of expertise.A powerful,extensible strategy of Distributed Artificial Intelligence (DAI) for overcoming such bounds is to put the system in a society of systems.So the ability to coordinate group activities of individuals and to communicate between each other is necessary for a language describing DAI systems.Agent-oriented language NUML is such a language.It is a specific kind of object-oriented language.To give formal semantics to NUML,there is the problem to formalise object-oriented programming paradigm which is still open.The theory of higher-order π-calculus is a concurrent computation model with sufficient capability,which provides us a mathematical tool to do the formalization.This paper tries to use higher-order π-calculus to formalise NUML.     

Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language

Complex software systems typically involve features like time, concurrency and probability, with probabilistic computations playing an increasing role. However, it is currently challenging to formalize languages incorporating all those features. Recently, the language PTSC has been proposed to integrate probability and time with shared-variable concurrency (Zhu et al. (2006, 2009) [51] and [53]), where the operational semantics has been explored and a set of algebraic laws has been investigated via bisimulation. This paper investigates the link between the operational and algebraic semantics of PTSC, highlighting both its theoretical and practical aspects.The link is obtained by deriving the operational semantics from the algebraic semantics, an approach that may be understood as establishing soundness of the operational semantics with respect to the algebraic semantics. Algebraic laws are provided that suffice to convert any PTSC program into a form consisting of a guarded choice or an internal choice between programs, which are initially deterministic. That form corresponds to a simple execution of the program, so it is used as a basis for an operational semantics. In that way, the operational semantics is derived from the algebraic semantics, with transition rules resulting from the derivation strategy. In fact the derived transition rules and the derivation strategy are shown to be equivalent, which may be understood as establishing completeness of the operational semantics with respect to the algebraic semantics.That theoretical approach to the link is complemented by a practical one, which animates the link using Prolog. The link between the two semantics proceeds via head normal form. Firstly, the generation of head normal form is explored, in particular animating the expansion laws for probabilistic interleaving. Then the derivation of the operational semantics is animated using a strategy that exploits head normal form. The operational semantics is also animated. These animations, which again supports to claim soundness and completeness of the operational semantics with respect to the algebraic, are interesting because they provide a practical demonstration of the theoretical results.     

一种基于规则的语言的公理语义

为了准确描述离散事件控制系统对象之间的逻辑关系和编写控制程序,提出了一种基于规则的语言——逻辑规则描述语言（LRDL）。用EBNF给出了LRDL的语法定义,基于Hoare逻辑的公理系统,形式化地给出并证明了LRDL的公理语义,为用LRDL编写的程序的正确性证明提供了理论依据。     

Translational Semantics for a Conceptual Level Query Language

A conceptual level database language for the entity relationship (ER) model implicitly contains integrities basic to ER concepts and special retrieval semantics for inheritances of attributes and relationships.Prolog,which belongs to the logical and physical level,cannot be used as a foundation to directly define the database language.It is shown how Prolog can be enhanced to understand the concepts of entities,relationships,attributes and is-a relationships.The enhanced Prolog is then used as a foundation to define the semantics of a database query language for the ER model.The three basic functions of model specification,updates and retrievals are defined.     

A layered semantics for a parallel object-oriented language

We develop a denotational semantics for POOL, a parallel object-oriented programming language. The main contribution of this semantics is an accurate mathematical model of the most important concept in object-oriented programming: the object. This is achieved by structuring the semantics in layers working at three different levels: for statements, objects and programs. For each of these levels we define a specialized mathematical domain of processes, which we use to assign a meaning to each language construct. This is done in the mathematical framework of complete metric spaces. We also define operators that translate between these domains. At the program level we give a precise definition of the observable input/output behaviour of a particular program, which could be used at a later stage to decide the issue of full abstractness. We illustrate our semantic techniques by first applying them to a toy language similar to CSP.This paper describes work done in ESPRIT Basic Research Action 3020,Integration.     

Denotational semantics of a synchronous VHDL subset

A denotational definition for a single clock synchronous subset of VHDL is proposed. The different domains for variables and signals, the elaboration of static environments, and the formulation of a simulation algorithm for the sub-language characterize this definition, and distinguish it from more traditional denotational semantics of programming languages.     

A formal semantics for debugging synchronous message passing-based concurrent programs

During a human-exoskeleton collaboration, the interaction torque on exoskeleton resulting from the human cannot be clearly determined and conducted by normal physical models. This is because the torque depends not only on direction and orientation of both human-operator and exoskeleton but also on the physical properties of each operator. In this paper, we present our investigations on the relationship between the interaction torques with the dynamic factors of the human-exoskeleton systems using state-of-the-art learning techniques （nonparametric regression techniques） and provide control applications based on the findings. Exper- imental data was collected from various human-operators when they were attached to the designed exoskeleton to perform unconstraint motions with and without control. The results showed that regardless of how the ex- periments were done and which learning method was chosen, the resulting interaction could be best represented by time varying non-linear mappings of the operator＇s angular position, and the exoskeleton＇s angular position, velocity, and acceleration during locomotion. This finding has been applied to advanced controls of the lower exoskeletal robots in order to improve their performance while interacting with human.     

A formal semantics for debugging synchronous message passing-based concurrent programs

In this paper, we propose a semantic framework to debug synchronous message passing-based con- current programs, which are increasingly useful as parallel computing and distributed systems become more and more pervasive. We first design a concurrent programming language model to uniformly represent exist- ing concurrent programming languages. Compared to sequential programming languages, this model contains communication statements, i.e., sending and receiving statements, and a concurrent structure to represent com- munication and concurrency. We then propose a debugging process consisting of a tracing and a locating procedure. The tracing procedure re-executes a program with a failed test case and uses specially designed data structures to collect useful execution information for locating bugs. We provide for the tracing procedure a struc- tural operational semantics to represent synchronous communication and concurrency. The locating procedure backward locates the ill-designed statement by using information obtained in the tracing procedure, generates a fix equation, and tries to fix the bug by solving the fix equation. We also propose a structural operational semantics for the locating procedure. We supply two examples to test our proposed operational semantics.