Exercise 12: Imperative Software Verification - A Deep Embedding

Define the Programming Language

Consider the following grammar for a simple imperative programming language that lacks a loop construct:

expression	::=	variable
	|	constant
	|	expression + expression
	|	expression - expression

boolean_expression	::=	expression = expression
	|	expression < expression
	|	!boolean_expression
	|	boolean_expression & boolean_expression
	|	boolean_expression | boolean_expression

command	::=	skip
	|	variable := expression
	|	command; command
	|	if boolean_expression then command else command

We would now like to define HOL data-types corresponding to expressions, boolean expressions, and commands. We will use HOL strings to represent variable names, so you will first need to load the HOL string library.

Since we don't often define new types in HOL, the type definition functions are found in a separately loadable module. Therefore, before we can make a type definition, we must load the module as follows:

load "Define_type";

We are now almost ready to define types corresponding to the nonterminals in the grammar above. Lets first consider how to define a type expression to represent expressions. We are going to use HOL strings to represent variable names. If `"max"' is a HOL term of type string, then it can't also be of type expression. To get around this we will use a constructor function `%' to make expressions from strings. For example, `%"max"' will be a term of type expression that represents a variable with the string `"max"' for its name. Similarly, we will represent the value of constants with HOL nums, and construct expressions from them with the function `#'.

Since we are going to use strings and nums in the HOL formalisation we will need to load the libraries numLib and stringLib.

A final obstacle remains to be cleared before we can define our HOL type for expressions. The symbols `+' and `-' have already been used for the standard arithmetic operators on nums and so aren't available for us to use in expressions. The good news is that nobody has used `++' and `--', so we will use those instead.

By this time, the actual grammar we will be able to implement for expressions looks like this.

expression	::=	%string
	|	#num
	|	expression ++ expression
	|	expression -- expression

This can now be captured directly with the following type definition:

 
val expression_AX = Define_type.define_type
    {name = "expression_AX",
     type_spec = `expression = % of string
                             | # of num
                             | ++ of expression => expression
                             | -- of expression => expression`,
     fixities = [Prefix, Prefix, Infix 1000, Infix 1000]};

The list called fixities describes the fixity of each of the constructors of the type in turn. Constructors can be either prefix or infix, and infix constructors have a binding power associated with them; the higher the number the tighter it binds.

Type definitions, like the one above, extend the HOL logic with a new axiom that describes the type. From this axiom, which is returned by the definition, it is possible derive theorems which allow recursive functions to be defined over the type and theorems to be proved about values of the type using induction.

Using this type definition as an example, define types to capture boolean expressions and commands as well.
Hint:

• The following symbols already have meanings in HOL terms `=', `<', `!', `|' and `;'. In each case, doubling the symbols will be OK (i.e., use `==' instead of `='.)
• You can't use `mix-fix' in HOL terms, so just use the syntax `if b c<sub>0</sub> c<sub>1</sub>' rather than `if b then c₀ else c₁'.
• Your infix constructors should have the following relative binding powers:

  strongest:		+, -
  		=, <
  		&, |
  		:=
  weakest:		;

Give the Language a Semantics

The abstract state of a computer will be represented as function from variables (strings) to values (numbers). In this model s v is the value of the variable v in the state s. The following definition describes a meaning function for expressions, Me, that takes expressions and maps them into functions from states to values.

val Me_DEF = new_recursive_definition
    {name = "Me_DEF",
     rec_axiom = expression_AX,
     def = 
     Term `
     (Me (% v) s = s v) /\  
     (Me (# c) s = c) /\  
     (Me (m ++ n) s = (Me m s) + (Me n s)) /\  
     (Me (m -- n) s = (Me m s) - (Me n s))`,
     fixity = Prefix};

Define a similar meaning function Mb that takes boolean expressions and maps them into functions from states to booleans.

Define a function update such that if s is a state (a function from variables to values ), v is string, and n is a value (a number), then update v n s is a new state in which the value of the variable named v is the number n and the values of all the other variables are as they were in state s.
Hint: Use a conditional expression.

Define another meaning function Mc for the meaning of commands. Mc should map commands into functions from initial states to final states.
Hint:

• This is simpler than the approach taken in the lecture where the meaning of a command was represented as a state relation. This is because the set of commands discussed in the lecture included a loop, which could fail to terminate and thus not produce any final state.
• Use your function update to define the meaning of assignment.
• Note that the definition will be made up of a number of equations, each of following form:

  Mc command parameters = ...

  Each clause must have the same number of parameters, and the right-hand side of the equation may not take the form of a lambda-abstraction.

Some Language Related Proofs

Prove that sequential composition is associative.
Hint: The conversion FUN_EQ_CONV could be helpful for this proof.

Consider the following fragment of code:

t := x; x := y; y := t

Prove that the value of the variable x after executing these commands is equal to the value of y before hand.
Hint: The string library, which you have loaded, contains a conversion string_EQ_CONV, which takes terms of the form "string1" = "string2" and decides whether or not the term is true. You will no doubt find it useful to use this conversion in the following tactic:

(CONV_TAC (DEPTH_CONV stringLib.string_EQ_CONV))