0 Introduction
We present formal operational semantics for the C programming language. Our starting point is the ANSI standard for C as described in [KR]. Knowledge of C is not necessary (though it may be helpful) for comprehension, since we explain all relevant aspects of C as we proceed.
Our operational semantics is based on evolving algebras. An exposition on evolving algebras can be found in the tutorial [Gu]. In order to make this paper self-contained, we recall the notion of a (sequential) evolving algebra in Sect. 0.1. Our primary concern here is with semantics, not syntax. Consequently,we assume that all syntactic information regarding a given program is available to us at the beginning of the computation (via static functions). Weintendedtocover all constructs of the C programming language, but not the C standard library functions (e.g. fprintf(), fscanf()). It is not dicult to extend our description of C to include any desired library function or functions.
Evolving algebra semantic speci cations maybe provided on several abstraction levels for the same language. Having several such algebras is useful, for one can examine the semantics of a particular feature of a programming language at the desired level of abstraction, with unnecessary details omitted. It also makes comprehension easier. We present a series of four evolving algebras, each a re nement of the previous one.
The nal algebra describes the C programming language in full detail.
0.1 Evolving Algebras
An evolving algebraAis an abstract machine. Here we restrict attention to sequential evolving algebras. Thesignature ofAis a ( nite) collection of function names, eachnamehaving a xed arity. A state of Ais a set, the superuniverse, together with interpretations of the function names in the signature. These interpretations are calledbasic functionsof the state. The superuniverse does not change asAevolves; the basic functions may.
Formally, a basic function of arityr(i.e. the interpretation of a function name of arityr)isanr-ary operation on the superuniverse. (We often use basic functions withr=0;such basic functions will be called distinguished elements.) But functions naturally arising in applications may be de ned only on a part of the superuniverse. Such partial functions are represented by total functions in the following manner.
The superuniverse contains distinct elements true, false, undef which allow us to deal with relations (viewed as binary functions with valuestrue orfalse) and partial functions (wheref(a)=undef meansf is unde ned at the tuple a). These three elements arelogical constants. Their names do not appear in the signature; this is similar to the situation in rst-order logic with equality where equality is a logical constant and the sign of equality does not appear in the signature. In fact, we use equality as a logical constantas well.
are not dynamic are calledstatic.Toallow our algebras to interact conveniently with the outside world,we also make use ofexternalfunctions within our algebra. External functions are syntactically static (that is, never changed by rules), but have their values determined by an oracle. Thus, an external function may have di erentvalues for the same arguments as the algebra evolves.
0.2 Acknowledgements
An earlier version of this paper appeared as a technical report [GH1]. We gratefully acknowledge comments made by on the original report byEgonBorger, Andre Burago, Martin J. D urst, Stefano Guerrini, Raghu Mani, Arnd Poetzsch-He ter, Dean Rosenzweig, and Marcus Vale, as well as comments in the errata made by Lars Ole Andersen, L. Douglas Baker, Arnd Poetzsch-He ter, Thomas Tsukada, and ChuckWallace.
1 Algebra One: Handling C Statements
Our rst evolving algebra models the control structures of C.
1.1 Some Basic Functions
A universetasks consists of elements representing tasks to be accomplished by the program interpreter. The notion of task is a general one:e.g., a task may be the execution of a statement, initialization of a variable,or the evaluation of an expression. The elements of this universe are dependent on the particular C program being executed by the abstract machine. It is often useful to mark a given task with tags indicating its nature. This gives rise to a universe oftags.
A distinguished elementCurTask: tasksindicates the current task. In order to execute tasks in the proper order, a static functionNextTask: tasks!tasks indicates the next task to be performed once the current task has been completed. A static functionTaskType: tasks!tags indicates the action to be performed by the task. A universeresultscontains values whichmay appear as the result of a computation.
1.2 Macro: Moveto
Often, we transfer control to a particular task, modifyingCurTaskto indicate the transfer of control. In Algebra Two, the rules for modifyingCurTaskwill change somewhat; in order to facilitate this change, we will use theMoveto(Task)macro each time that we wish to transfer control. For now, the de nition of Moveto(Task)is shown in Fig. 1.
Si le lien ne fonctionne pas correctement, veuillez nous contacter (mentionner le lien dans votre message)The semantics of the C programming language (433 KO) (Cours PDF)
