scholarly journals Mathematical Foundation of A Semantic Directed Compiler Generator

1982 ◽  
Vol 11 (148) ◽  
Author(s):  
Henning Christiansen ◽  
Neil D. Jones
Keyword(s):  
Control Flow ◽  
Target Language ◽  
Full Detail ◽  
Formal Description ◽  
Mathematical Foundation ◽  
Correctness Proof ◽  
Compiler Generation ◽  
Language Semantics ◽  
Technical Details ◽  
Flow Treatment

<p>This paper describes technical details which were not included in the paper ''Control Flow Treatment in a Simple Semantics-Directed Compiler Generator'', presented at the IFIP working conference on Formal Description of Programming Concepts, Germany, 1982, due to lack of space. The present paper cannot be read separately.</p><p>We describe our method in full detail, including the <em>iterate</em>-operator in the S-algebra. Furthermore we give complete formal descriptions of the semantic algebra S and its models (Section 1), the compiler generation function d^c and the compile time interpretation J (Section 2), the target language semantics (Section 3), and in Section 4 the correctness proof.</p>

scholarly journals Control Flow Treatment in a Simple: Semantics-Directed Compiler Generator

1981 ◽  
Vol 10 (137) ◽  
Author(s):  
Neil D. Jones ◽  
Henning Christiansen
Keyword(s):  
Simple Algebra ◽  
Control Flow ◽  
Program Execution ◽  
Correctness Proofs ◽  
Compiler Generation ◽  
Source Program ◽  
Target Program ◽  
Definition Of ◽  
Flow Treatment ◽  
Semantic Definition

<p>A simple algebra-based algorithm for compiler generation is described. Its input is a semantic definition of a programming language, and its output is a ''compiling semantics'' which maps each source program into a sequence of compile-time actions whose net effect on execution is the production of a semantically equivalent target program. The method does not require individual compiler correctness proofs or the construction of specialized target algebras.</p><p>Source program execution is assumed to proceed by performing a series of elementary actions on a runtime state. A semantic algebra is introduced to represent and manipulate possible execution sequences. A source semantic definition has two parts: A set of semantic equations mapping source programs into terms of the algebra, and an interpretation which gives concrete definitions of the state and the elementary actions on it.</p>

Specification and Verification of the ATMR Protocol Using UNITY: Part 1: Modeling and Specification of the Protocal

1998 ◽  
Vol 08 (04) ◽  
pp. 421-432 ◽  
Author(s):  
Michel Charpentier ◽  
Gérard Padiou
Keyword(s):  
Quality Assurance ◽  
Temporal Logic ◽  
Development Process ◽  
Detection Algorithm ◽  
Formal Description ◽  
General Development ◽  
Correctness Proof ◽  
Program Specification ◽  
Specification And Verification

We propose a description and validation of the ATMR protocol within the UNITY formalism. This formal description helps us understand precisely the mechanisms this protocol involves. In particular, we have noted the use of an incorrect detection algorithm to generate reset slots. In this first part, we provide an operational description using the UNITY programming notation as well as a specification of the main correctness properties in the UNITY temporal logic. A second part [2] is dedicated to a hand-made correctness proof. The proof shows that the model satisfies the specification despite this spurious detection. In this study, we apply a general development process based upon the UNITY formalism. During this process, we tune the program specification in order to make the later validation step easier, in the same way as the inclusion of traces, breakpoints, and assertions prepares a program for its quality assurance tests.

scholarly journals A First-Order One-Pass CPS Transformation

2001 ◽  
Vol 8 (49) ◽  
Author(s):  
Olivier Danvy ◽  
Lasse R. Nielsen
Keyword(s):  
Control Flow ◽  
Logical Relation ◽  
Correctness Proof ◽  
First Order ◽  
Structural Induction ◽  
Flow Information

We present a new transformation of call-by-value lambda-terms into continuation-passing style (CPS). This transformation operates in one pass and is both compositional and first-order. Because it operates in one pass, it directly yields compact CPS programs that are comparable to what one would write by hand. Because it is compositional, it allows proofs by structural induction. Because it is first-order, reasoning about it does not require the use of a logical relation.<br /> <br />This new CPS transformation connects two separate lines of research. It has already been used to state a new and simpler correctness proof of a direct-style transformation, and to develop a new and simpler CPS transformation of control-flow information.

FORMAL METHOD FOR AUTOMATED TRANSFORMATION OF LOTOS SPECIFICATIONS TO ESTELLE SPECIFICATIONS

2005 ◽  
Vol 15 (05) ◽  
pp. 873-891 ◽  
Author(s):  
HAZEM EL-GENDY ◽  
NABIL EL-KADHI
Keyword(s):  
Real Time ◽  
Formal Method ◽  
Conformance Testing ◽  
Control Flow ◽  
Semantic Model ◽  
Formal Description ◽  
Real Time Systems ◽  
Behavior Tree ◽  
Time Systems ◽  
Formal Description Techniques

ISO and IEC have jointly developed two Formal Description Techniques (FDTs) for specifying distributed real time systems such as computer/telecommunications protocols. These are Lotos and Estelle. In this paper, a formal method for automated transformation of a Lotos specification to an Estelle specification is presented. The method is applicable to various Lotos specification styles and to various communications protocols of ISO OSI layers. Our method has applications in conformance testing of such systems and building common semantic model for the various FDTs. In this paper, we develop an algorithm for constructing a 'Data Oriented'-Restricted Behavior Tree T that represent both the control flow aspects and the data flow aspects of the system. Then, we develop an algorithm for constructing the Estelle specifications from T. A minimization rule is also developed to optimize the size of the Estelle specification by reducing both the number of states and the number of transitions.

scholarly journals Abstract Semantic Algebras!

1982 ◽  
Vol 11 (145) ◽  
Author(s):  
Peter D. Mosses
Keyword(s):  
Programming Languages ◽  
Programming Language ◽  
Conceptual Analysis ◽  
Formal Description ◽  
Data Types ◽  
New Approach ◽  
Initial Algebra ◽  
Language Semantics ◽  
Abstract Data ◽  
Initial Algebra Semantics

A new approach to the formal description of programming language semantics is described and illustrated. ''Abstract semantic algebras'' are just algebraically-specified abstract data types whose operations correspond to fundamental concepts of programming languages. The values of abstract semantic algebras are taken as meanings of programs in Denotational (or Initial Algebra) Semantics, instead of using Scott domains. This leads to semantic descriptions that clearly exhibit the underlying conceptual analysis, and which are rather easy to modify and extend. Some basic abstract semantic algebras corresponding to fundamental concepts of programming languages are given; they could be used in the description of many different programming languages.

Specification and Verification of the ATMR Protocol Using UNITY: Part 2: Correctness Proof

1998 ◽  
Vol 08 (04) ◽  
pp. 433-445 ◽  
Author(s):  
Michel Charpentier ◽  
Gérard Padiou
Keyword(s):  
Temporal Logic ◽  
Detection Algorithm ◽  
Generation Mechanism ◽  
Formal Description ◽  
Correctness Proof ◽  
Previous Part ◽  
Specification And Verification

We propose a description and validation of the ATMR protocol within the UNITY formalism. This formal description helps us understand precisely the mechanisms this protocol involves. In particular, we have noted the use of an incorrect detection algorithm to generate reset slots. An operational description using the UNITY programming notation and a specification of the main correctness properties in the UNITY temporal logic are given in a previous part [2]. This second part is dedicated to a hand-made correctness proof. The proof shows that the model satisfies the specification despite the spurious detection in the reset generation mechanism.

scholarly journals A Formal, Resource Consumption-Preserving Translation from Actors with Cooperative Scheduling to Haskell*

2020 ◽  
Vol 177 (3-4) ◽  
pp. 203-234
Author(s):  
Elvira Albert ◽  
Nikolaos Bezirgiannis ◽  
Frank de Boer ◽  
Enrique Martin-Martin
Keyword(s):  
Cost Model ◽  
Formal Semantics ◽  
Operational Semantics ◽  
Resource Consumption ◽  
Target Language ◽  
Correctness Proof ◽  
High Level ◽  
Resource Aware ◽  
The Cost ◽  
Cooperative Scheduling

We present a formal translation of a resource-aware extension of the Abstract Behavioral Specification (ABS) language to the functional language Haskell. ABS is an actor-based language tailored to the modeling of distributed systems. It combines asynchronous method calls with a suspend and resume mode of execution of the method invocations. To cater for the resulting cooperative scheduling of the method invocations of an actor, the translation exploits for the compilation of ABS methods Haskell functions with continuations. The main result of this article is a correctness proof of the translation by means of a simulation relation between a formal semantics of the source language and a high-level operational semantics of the target language, i.e., a subset of Haskell. We further prove that the resource consumption of an ABS program extended with a cost model is preserved over this translation, as we establish an equivalence of the cost of executing the ABS program and its corresponding Haskell-translation. Concretely, the resources consumed by the original ABS program and those consumed by the Haskell program are the same, considering a cost model. Consequently, the resource bounds automatically inferred for ABS programs extended with a cost model, using resource analysis tools, are sound resource bounds also for the translated Haskell programs. Our experimental evaluation confirms the resource preservation over a set of benchmarks featuring different asymptotic costs.

Design of Tiny TTY for Multi-Process Micro-Kernel Embedded OS on ARM

2013 ◽  
Vol 760-762 ◽  
pp. 1677-1683
Author(s):  
Bo Qu
Keyword(s):  
Operating System ◽  
Data Structures ◽  
Colleges And Universities ◽  
Control Flow ◽  
Embedded Operating System ◽  
System Research ◽  
Tool Chain ◽  
Embedded Os ◽  
Design And Implementation ◽  
Technical Details

This paper describes the design and implementation of tiny TTY driver for ARM based multi-process micro-kernel embedded operating system in technical details, including overview of TTY (Control flow of terminal driver, process modes for TTY, data structures for tiny TTY), interrupt-mode UART driver, and tiny TTY driver for micro-kernel OS. The ARM based operating system is designed and implemented by the author of this paper on Linux with GNU tool chain. Based on the TTY, some shell commands are designed, in which the key strokes on the super terminal are read as the input of the commands analogous to the case for ordinary embedded Linux. On the premise of implementing essential functions, the routines for the tiny TTY is designed as simple as possible therefore it is suited to not only embedded operating system research but also embedded related curriculum teaching in colleges and universities.

A Completely Verified Realistic Bootstrap Compiler

2003 ◽  
Vol 14 (04) ◽  
pp. 659-680 ◽  
Author(s):  
Axel Dold ◽  
Friedrich von Henke ◽  
Wolfgang Goerigk
Keyword(s):  
Research Effort ◽  
Target Language ◽  
A Posteriori ◽  
Correctness Criterion ◽  
Language Semantics ◽  
German Research ◽  
Verification Process ◽  
High Level ◽  
First Time ◽  
Real Target

This paper reports on a large verification effort in constructing an initial fully trusted bootstrap compiler executable for a realistic system programming language and real target processor. The construction and verification process comprises three tasks: the verification of the compiling specification (a relation between abstract source and target programs) with respect to the language semantics and a realistic correctness criterion. This proof has been completely mechanized using the PVS verification system and is one of the largest case-studies in formal verification we are aware of. Second, the implementation of the specification in the high-level source language following a transformational approach, and finally, the implementation and verification of a binary executable written in the compiler's target language. For the latter task, a realistic technique has been developed, which is based on rigorous a-posteriori syntactic code inspection and which guarantees, for the first time, trusted execution of generated machine programs. The context of this work is the joint German research effort Verifix aiming at developing methods for the construction of correct compilers for realistic source languages and real target processors.

scholarly journals The Sun RPC Language Semantics

2002 ◽  
Vol 21 (419) ◽  
Author(s):  
Martin Musicante
Keyword(s):  
Formal Specification ◽  
The Sun ◽  
Formal Description ◽  
Remote Procedure Call ◽  
Procedure Call ◽  
Communication Mechanism ◽  
Language Semantics

A formal description of the Sun Remote Procedure Call Protocol is given. The description is written using the Action Notation style of formal specification. Action Notation proves to be adequate to express the meaning of the Sun RPC communication mechanism.

Sign in / Sign up

Export Citation Format

Share Document