Index
Blog

# Project 2

Following are some test cases that I’ve used for past model checking assignments. All are simple imperative programs written in a canonical block oriented style that everyone should recognize. For this project you should take each program, define a correctness invariant, and verify the correctness invariant by hand and/or using the model_check capability and small-step operational semantics defined by Chlipala. The first two should be simple as they involve no iteration. Be careful with the nested WHILE loop if you use model_check.

You may work together on these problems and we will discuss in class.

IF X <= 3 THEN IF Y <= 4 THEN Z:=X+Y
ELSE SKIP
ELSE IF Y <= 4 THEN Z:=X*Y
ELSE Z:=1

X := 1 ;
IF X = 3 THEN X:=1 ; Y:=4 ELSE X:=0 ENDIF ;
SKIP

Y:=0;
IF X <= 10 THEN WHILE Y <= 10 DO Y:=Y+1; X:=X+Y
ELSE X := 10

Y := X ;
Z := Y ;
WHILE Y <= 10 DO
WHILE Z <= 10 DO
X := X+Z ;
Z := Z+1 ;
Y := Y+1 ;
SKIP ;