SmallC Formal Operational Semantics
Spring 2018
1 Introduction
This document presents a formal semantics of Small C. It has two main parts. The first part is the expression semantics. It corresponds to the implementation of your eval expr function. The second part is the statement semantics. It corresponds to the implementation of your eval stmt function.
2 Preliminaries
2.1. Environments. Both parts define judgments that make use of en- vironments A. The rules show two operations on environments:
• A(x) means to look up the value of x maps to in the environment A. This operation is undefined if there is no mapping for x in A. We write · for the empty environment. Lookup on this environment is always undefined; i.e., ·(x) is undefined for all x.
• The second operation is written A[x → v]. It defines a new environment that is the same as A but maps x to v. It thus overrides any prior mapping for x in A. This is similar to the “concatenation” of environments shown in the lecture notes from Feb. 28. So, ·[x → 1] is an environment that maps x to 1 but is undefined for all other variables. The environment ·[x → 1][y → 2] is an environment that maps x to 1 and y to 2. As such, ifA=·[x→1][y→2]thenA(x)=1. Thatis,lookingupxinthesecond example environment produces its mapped-to value, 1.
2.2. Syntax. In this document, we have simplified the presentation of the syntax, so it may not correspond exactly to the files that your interpreter will read in. For example, we write while e s to represent the syntax of a while- loop, where e is the guard and s is the body. This corresponds to While of expr * stmt in the types.ml file. Hopefully the connection between what we show here at that file is clear enough from context.
1
2.3. Error conditions. The semantics here defines only correct evalu- ations. It says nothing about what happens when, say, you have a type error. For example, for the rules below there is no value v for which you can prove the judgment ·; 1 + true −→ v. In your actual implementation, erroneous programs will cause an exception to be raised, as indicated in the project README.
3 Expression Semantics
This part of the formal semantics corresponds to the implementation of your eval expr function. That function has type environment -> expr -> value. In the semantics, we write the judgment A;e −→ v, where A represents the environment, e represents the expression, and v represents the final value. This follows the same format as the lecture notes from February 28.
3.1. Abstract syntax grammar. Expressions and values are defined by the following grammar:
Integers
Booleans
Values
Expressions e ::= v|!e|e⊕e|e⊙e|e==e|e!=e
n is any integer b ::= true | false v ::= n|b
Here, we write ⊕ to represent any operator involving a pair of integers. This could be addition (+), comparison (≤), multiplication (×), etc. We write ⊙ to represent any operator involving a pair of booleans. This could be boolean-and (&&), boolean-or (||), etc. We do not go into specifics here about what these actually do; they should match your intuition.
3.2. Rules. Here are the axioms. A(x) = v
Id A;x−→v Int A;n−→n
Bool-True A; true −→ true Bool-False A; false −→ false
Here are the rest of the rules for expressions.
2
Eq-True
NotEq-True
A;e1 −→v
A; e2 −→ v A;e1 == e2 −→ true
A;e1 −→v1
A;e2 −→v2
v1 is different than v2 A;e1 !=e2 −→true
Eq-False
A;e1 −→v1
A;e2 −→v2
v1 is different than v2 A;e1 == e2 −→ false
A;e1 −→v
A; e2 −→ v A;e1 !=e2 −→false
A;e1 −→b1 A;e2 −→b2
b3 is b1 ⊙ b2 A;e1 ⊙e2 −→b3
BinOp-Int
A;e1 −→n1 A;e2 −→n2
v is n1 ⊕ n2 A;e1 ⊕e2 −→v
Unary-Not
NotEq-False
BinOp-Bool
A;e1 −→b1 b2 is ¬b1 A;!e1 −→b2
4 Statement Semantics
This part of the formal semantics corresponds to the implementation of your
eval stmt function. That function has type environment -> stmt -> environment. In the semantics, we write the judgment A;s −→ A′, where A represents the
input environment, s represents the statement to execute, and A′ represents the
final output environment. Statements are different from expressions in that they
do not “return” anything themselves; instead, their impact occurs by modifying
the environment (by assigning to variables).
4.1. Abstract syntax grammar. Statements are defined by the follow- ing grammar:
Statements s ::= skip|s;s|ifess|whilees|intx|boolx|x=e In the project itself there is also a statement form for printing; we leave that
out of the formal semantics.
4.2. Rules.
Variables. In Small C, you have to declare a variable, with its type, before you use it. When declared, it will be initialized to a default value. You cannot declare the same variable twice.
3
Declare-Int
A(x) is not defined A;int x −→ A[x → 0]
Declare-Bool
A(x) is not defined A;bool x −→ A[x → false]
Assigning to variables must respect their declared type. In particular, you cannot assign to a variable you have not declared, and you cannot write a boolean to a variable declared as an int, or vice versa.
Assign-Int
Control Flow.
Nop
Assign-Bool
If-True
While-True
If-False
A;e −→ false A;s2 −→A2 A;if es s −→ A
A(x) = n (for some n) A ; e −→ n 1
A(x) = b (for some b) A ; e −→ b 1
A ; x = e −→ A [ x → b 1 ] Here are the rules for the different control flow constructs.
A ; x = e −→ A [ x → n 1 ]
A; skip −→ A
A;e −→ true
A;s1 −→A1
Sequence
A;s1 −→A1 A1;s2 −→A2 A; s1; s2 −→ A2
A;if es s −→ A
121 122
A; e −→ true
A ; s −→ A 1 A1;while es −→ A2
While-False
A;e −→ false A; while e s −→ A
A;s −→ A1 A1; e −→ false
DoWhile-True
2
A ; s −→ A 1
A1;e −→ true
A1; dowhile s e −→ A2
DoWhile-False
A; while e s −→ A
A; dowhile s e −→ A
A; dowhile s e −→ A 21
4