This homework is important, it may carry more points than others. For this homework only, you can do it in groups of 2 and hand in only one solution per group, but write down the name of others that you worked with.
We consider a small language that contains the x^y operator. Our goal is to design a system where x^y is never evaluated for negative y.
We have the following types:
- Pos <: Int (Pos is a subtype of Int)
- Ref[Int], Ref[Pos]
In scala, Ref[T] would look like this:
References are explained in Subtyping with Assignment and Generics
Expressions are built (non-recursively) from:
- integer constants
- binary operators , , ^
- variable.content expressions
More precisely, the grammar of expressions e is:
e ::= cvar | cvar + cvar | cvar * cvar | cvar ^ cvar | cvar.content cvar ::= var | constant
Assignment statements are the only statements. They have an expression on their right hand side and their left hand side is given by the following grammar:
lhs ::= var | var.content
A program is simply a sequence of variable declarations, followed by a sequence of assignments. Example:
x : Ref[Int] y : Ref[Pos] z : Int
x.content = 3 x = y y.content = x.content
The typing rules for and ^ are:
Note that e.g. a derivation
follows from the above rules and the subtyping rule Pos <: Int, because we have a general rule
Give type checking rules that express properties of multiplication * , referring only to types Int and Pos. Your rules should be as precise as possible, but they should refer only to types of sub-expressions, not to their values.
The initial type environment is built according to declarations. For each
var x : T
we have in the environment.
To type-check a program, we use the rule
Give the remaining
- type checking rules (when is an assignment well-typed?), and
- subtyping rules (in addition to Pos <: Int) for statements and their expressions, including rules for Ref[Int] and Ref[Pos].
Because we have assignment, we'll use an evaluation environment in the semantics of evaluation. Our environment will contain two kinds of things: mappings for variables and mapping for cells. A variable is mapped to an Int, Pos, or cell. A cell is mapped to an Int or Pos. Cells are like addresses in a memory.
We need to create an initial evaluation environment according to the initial declarations. Our convention is to initialize variables of type Int to 0 and Pos to 1. References are initialized to fresh cells.
x : Ref[Int] y : Ref[Pos] z : Pos
Let us now give operational semantics for our language:
We define to be the function that evaluates an expression in evaluation environment :
We have two evaluation rules:
We will define the notion that program state type checks, by saying that both the program and the state type check in :
Here is what you defined in b)-subtyping. Now, define , which, intuitively, will check that the values of variables and reference cells make sense according to types. (In principle, any definition here is acceptable as long as your proof in d)-good and e)-induction work. You may need to revisit this part if d) or e) do not work.)
Show that if and the program starts with the statement
x = y ^ z
then is a positive integer. (This is desirable so that the evaluation of ^ does not crash.)
Show that if the program and evaluation environment type check and we execute one assignment statement, the program and the environment again type check in the new environment i.e.
Explain why c),d),e) taken together imply that, no matter what the program is, if it type checks, then its execution from the initial state will never attempt to evaluate x^y for a negative value of y.
Note that this property would continue to hold if we added loops and jumps to our language.
Suppose we change the rules so that
Ref[Pos] <: Ref[Int]
Show that f)-safety does not hold any more, that is, give an example of a well-typed program whose execution crashes due to ^ being applied to a negative number.
If you take the same definition of as in d), prove or disprove that the claim in e) holds in the presence of the new subtyping rule Ref[Pos] <: Ref[Int]. If you prove the claim, the proof should follow the structure as in e), if you disprove the claim, you should give an example and for which e) does not hold.