“What is an algorithm?” is a fundamental question of computer science. Gurevich’s behavioural theory of sequential algorithms (aka the sequential ASM thesis) gives a partial answer by defining (non-deterministic) sequential algorithms axiomatically, without referring to a particular machine model or programming language, and showing that they are captured by (nondeterministic) sequential Abstract State Machines (nd-seq ASMs). However, recursive algorithms such as mergesort are not covered by this theory, as has been pointed out by Moschovakis, who had independently developed a different framework to mathematically characterize the concept of (in particular recursive) algorithm. In this article we propose an axiomatic definition of the notion of sequential recursive algorithm which extends Gurevich’s axioms for sequential algorithms by a Recursion Postulate and allows us to prove that sequential recursive algorithms are captured by recursive Abstract State Machines, an extension of nd-seq ASMs by a CALL rule. Applying this recursive ASM thesis yields a characterization of sequential recursive algorithms as finitely composed concurrent algorithms all of whose concurrent runs are partial-order runs.

Journal Article The abstract state machines method for modular design and analysis of programming languages Get access Egon Börger Egon Börger Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 27, Issue 2, March 2017, Pages 417–439, https://doi.org/10.1093/logcom/exu077 Published: 18 December 2014 Article history Received: 26 May 2013 Published: 18 December 2014

A concurrent Abstract State Machine (ASM) is a family of agents each equipped with a sequential ASM to execute. We define the semantics of concurrent ASMs by concurrent ASM runs which overcome the problems of Gurevich’s distributed ASM runs and generalize Lamport’s sequentially consistent runs. A postulate characterizing an intuitive understanding of concurrency is formulated. It allows us to state and prove an extension of the sequential ASM thesis to a concurrent ASM thesis.

We define a programming language independent controller TaCtl for multi-level transactions and an operator TA, which when applied to concurrent programs with multi-level shared locations containing hierarchically structured complex values, turns their behavior with respect to some abstract termination criterion into a transactional behaviour. We prove the correctness property that concurrent runs under the transaction controller are serialisable, assuming an Inverse Operation Postulate to guarantee recoverability. For its applicability to a wide range of programs we specify the transaction controller TaCtl and the operator TA in terms of Abstract State Machines (ASMs). This allows us to model concurrent updates at different levels of nested locations in a precise yet simple manner, namely in terms of partial ASM updates. It also provides the possibility to use the controller TaCtl and the operator TA as a plug-in when specifying concurrent system components in terms of sequential ASMs.

No abstract available.

Abstract We explain why for the verified software challenge proposed in Hoare (J ACM 50(1): 63–69, 2003), Hoare and Misra (Verified software: theories, tools, experiments. Vision of a Grand Challenge project. In: [Meyer05]) to gain practical impact, one needs to include rigorous definitions and analysis, prior to code development and comprising both experimental validation and mathematical verification, of ground models , i.e., blueprints that describe the required application-content of programs. This implies the need to link via successive refinements the relevant properties of such high-level models in a traceable and checkable way to code a compiler can verify. We outline the Abstract State Machines (ASM) method, a discipline for reliable system development which allows one to bridge the gap between informal requirements and executable code by combining application-centric experimentally validatable system modelling with mathematically verifiable stepwise detailing of abstract models to compile-time-verifiable code.

We propose a structured mathematical definition of the semantics of C♯ programs to provide a platform-independent interpreter view of the language for the C♯ programmer, which can also be used for a precise analysis of the ECMA standard of the language and as a reference model for teaching. The definition takes care to reflect directly and faithfully—as much as possible without becoming inconsistent or incomplete—the descriptions in the C♯ standard to become comparable with the corresponding models for Java in Stärk et al. (Java and Java Virtual Machine—Definition, Verification, Validation, Springer, Berlin, 2001) and to provide for implementors the possibility to check their basic design decisions against an accurate high-level model. The model sheds light on some of the dark corners of C♯ and on some critical differences between the ECMA standard and the implementations of the language.

Abstract In this paper the abstract state machine (ASM) refinement method is presented. Its characteristics compared to other refinement approaches in the literature are explained. Some frequently occurring forms of ASM refinements are identified and illustrated by examples from the design and verification of architectures and protocols, from the semantics and the implementation of programming languages and from requirements engineering.

We provide a rigorous framework for language and platform independent design and analysis of exception handling mechanisms in modern programming languages and their implementations. To illustrate the practicality of the method we develop it for the exception handling mechanism of Java and show that its implementation on the Java Virtual Machine (JVM) Is correct. For this purpose we define precise abstract models for exception handling in Java and in the JVM and define a compilation scheme of Java to JVM code which allows us to prove that, in corresponding runs, Java and the JVM throw the same exceptions and with equivalent effect. Thus, the compilation scheme can, with reasonable confidence, be used as a standard reference for Java exception handling compilation.

Starting from the textbook formulation of the tableau calculus we give an operational description of the tableau method in terms of abstract state machines at various levels of refinement ending after four stages at a specification that is very close to the lean TAP implementation of the tableau calculus in PROLOG. Proofs of correctness and completeness of the refinement steps are given.

This paper contributes to the development of a rigorous mathematical framework for the study of provably correct compilation techniques. The proposed method is developed through an implementation of a real-life non-toy imperative programming language with non-determinism and parallelism, i.e. Occam, to a commercial machine, namely the Transputer. We provide a mathematical definition of the Transputer Instruction Set architecture for executing Occam together with a correctness proof for a general compilation schema of Occam programs into Transputer code. We start from the ground model, an abstract processor, running a high and a low priority queue of Occam processes, which formalizes the semantics of Occam at the abstraction level of atomic Occam instructions. We develop here increasingly more refined levels of Transputer semantics, proving correctness (and when possible also completeness) for each refinement step. Along the way we collect our proof assumptions, a set of natural conditions for a compiler to be correct, thus making our proof applicable to a large class of compilers. As a by-product our construction provides a challenging realistic case study for proof verification by theorem provers.

Abstract We provide a mathematical specification of an extension of Warren's Abstract Machine (WAM) for executing Prolog to type-constraint logic programming and prove its correctness. Our aim is to provide a full specification and correctness proof of a concrete system, the PROTOS Abstract Machine (PAM), an extension of the WAM by polymorphic order-sorted unification as required by the logic programming language PROTOS-L. In this paper, while leaving the details of the PAM's type constraint representation and solving facilities to a sequel to this work, we keep the notion of types and dynamic type constraints abstract to allow applications to different constraint formalisms like Prolog III or CLP(R). This generality permits us to introduce modular extensions of Börger's and Rosenzweig's formal derivation of the WAM. Since the type constraint handling is orthogonal to the compilation of predicates and clauses, we start from type-constraint Prolog algebras with compiled AND/OR structure that are derived from Börger's and Rosenzweig's corresponding compiled standard Prolog algebras. The specification of the type-constraint WAM extension is then given by a sequence of evolving algebras, each representing a refinement level, and for each refinement step a correctness proof is given. Thus, we obtain the theorem that for every such abstract type-constraint logic programming system L, every compiler to the WAM extension with an abstract notion of types which satisfies the specified conditions, is correct.

Abstract We refine the mathematical specification of a WAM extension to typeconstraint logic programming given in [BeB96]. We provide a full specification and correctness proof of the PROTOS Abstract Machine (PAM), an extension of the WAM by polymorphic order-sorted unification as required by the logic programming language PROTOS-L, by refining the abstract type constraints used in [BeB96] to the polymorphic order-sorted types of PROTOS-L. This allows us to develop a detailed and mathematically precise account of the PAM's compiled type constraint representation and solving facilities, and to extend the correctness theorem to compilation on the fully specified PAM.

We present a design approach which allows us to formally specify a real-life processor as composed out of its basic architectural (formally specified) components. The methodology provides means to rely upon hierarchical refinements and modular structuring of the specifications as a discipline to control the behaviour of complex units in terms of the behaviour of their components. In particular this enables us to prove interesting dynamic properties about the processor in terms of properties of its basic architectural components. We have developed the method to accomplish a reverse engineering project for the VLSI implemented microprocessor zCPU, the controller of the successful APE100 massively parallel machine.

Abstract A Krom formula of pure quantification theory is a formula in conjunctive normal form such that each conjunct is a disjunction of at most two atomic formulas or negations of atomic formulas. Every class of Krom formulas that is determined by the form of their quantifier prefixes and which is known to have an unsolvable decision problem for satisfiability is here shown to be a conservative reduction class. Therefore both the general satisfiability problem, and the problem of satisfiability in finite models, can be effectively reduced from arbitrary formulas to Krom formulas of these several prefix types.