TypeCheckImpl:
PROGRAM
IMPORTS Atom, Unparser
EXPORTS TypeCheck = BEGIN
OPEN TypeCheck;
-- Some Atoms used as operators.
arrow : ATOM = Atom.MakeAtom [ "=>" ];
asgn : ATOM = Atom.MakeAtom[ "←" ];
box : ATOM = Atom.MakeAtom[ "||" ];
colon : ATOM = Atom.MakeAtom [ ":" ];
comma : ATOM = Atom.MakeAtom[ "," ];
dblEq : ATOM = Atom.MakeAtom[ "==" ];
eq : ATOM = Atom.MakeAtom[ "=" ];
ge : ATOM = Atom.MakeAtom[ ">=" ];
gt : ATOM = Atom.MakeAtom[ ">" ];
lbrace : ATOM = Atom.MakeAtom[ "{" ];
lbracket : ATOM = Atom.MakeAtom[ "[" ];
le : ATOM = Atom.MakeAtom[ "<=" ];
lparen : ATOM = Atom.MakeAtom [ "(" ];
lt : ATOM = Atom.MakeAtom[ "<" ];
minus : ATOM = Atom.MakeAtom[ "-" ];
ne : ATOM = Atom.MakeAtom[ "#" ];
not : ATOM = Atom.MakeAtom[ "~" ];
plus : ATOM = Atom.MakeAtom[ "+" ];
rbrace : ATOM = Atom.MakeAtom[ "}" ];
rbracket : ATOM = Atom.MakeAtom[ "]" ];
rparen : ATOM = Atom.MakeAtom[ ")" ];
semicolon : ATOM = Atom.MakeAtom[";"];
star : ATOM = Atom.MakeAtom[ "*" ];
up : ATOM = Atom.MakeAtom[ "^" ];
Wlp: PUBLIC PROCEDURE [ s : Stmt, p : Predicate ] RETURNS [ q : Predicate ] =
{
-- We calculate the weakest liberal precondition (wlp) of a statement S and a predicate P; it is the weakest predicate Q such that if you start S in state Q and S halts (i.e., doesn't abort or run forever) then P is true afterwards.
IF s = NIL THEN ERROR;
SELECT Optr [ s ]
FROM
asgn => q ← Substitute [ VarOfAsgn [ s ], Arg2 [ s ], p ];
semicolon => q ← Wlp [ Arg1 [ s ], Wlp [ Arg2 [ s ], p ] ];
$if => q ← WlpIfCmdList [ GcmdsOfIf [ s ], p ];
$do => q ← WlpDo [ s, p ];
ENDCASE => ERROR;
};
Substitute:
PRIVATE PROCEDURE [ v : Term, t : Term, p : ParseTree ] RETURNS [ q : ParseTree ] =
{
-- Substitute terms t for variables v in parse tree p. Note that t and v are either individual terms or lists separated by commas.
IF p = NIL THEN RETURN [ p ];
WITH p
SELECT
FROM
a : ATOM => q ← SubstituteForVar [ v, t, a ];
n : REF INT => q ← n;
l : List =>
q ←
CONS
[ Substitute [ v, t, l.first ], NARROW [ Substitute [ v, t, l.rest ], List ] ]
ENDCASE => ERROR;
};
SubstituteForVar:
PRIVATE PROCEDURE [ v : Term, t : Term, a : ATOM ] RETURNS [ q : ParseTree ] =
{
-- If the atom a is among the variables v, then substitute the corresponding term from t for it. Note that t and v are either individual terms or lists separated by commas.
IF v = NIL THEN RETURN [ a ];
IF
ISTYPE [ v,
ATOM ]
THEN
IF NARROW [ v, ATOM ] = a THEN RETURN [ t ] ELSE RETURN [ a ];
IF ( a =
NARROW [ Arg1 [ v ],
ATOM ] )
THEN
q ← Arg1 [ t ]
ELSE
q ← SubstituteForVar [ Arg2 [ v ], Arg2 [ t ], a ];
};
WlpIfCmdList:
PRIVATE PROCEDURE [ gcs : ParseTree, p : Predicate ] RETURNS [ q : Predicate ] =
{
-- We take the guarded commands of an if ... fi and return the and of their wlp's.
moreThanOne : BOOL; -- TRUE if there is more than one guard in the list.
wlpFirst, wlpRest : ParseTree; -- wlp's of first and other guards of the list.
IF gcs = NIL THEN RETURN [ $true ];
IF ( moreThanOne ← ( Optr [ gcs ] = box ) ) THEN
{
wlpFirst ← WlpIfCmd [ Arg1 [ gcs ], p ];
wlpRest ← WlpIfCmdList [ Arg2 [ gcs ], p ];
q ← Binary [ $and, Parenthesize [ wlpFirst ], wlpRest ]
}
ELSE
q ← Parenthesize [ WlpIfCmd [ gcs, p ] ];
};
WlpIfCmd:
PRIVATE PROCEDURE [ gc : Stmt, p : Predicate ] RETURNS [ q : Predicate ] =
{
-- We have a guarded command of the form G => S where G is a guard. If G is R, return ( R impl wlp(S,P) ). If G is of the form x : R, return all x : ( R impl wlp(S,P) ).
x, R, S : ParseTree; -- as above.
impl : ParseTree; -- the tree ( R impl wlp(S,P)).
IF gc = NIL OR Optr [ gc ] # arrow THEN ERROR;
[ x, R, S ] ← SplitGcmd [ gc ];
impl ← PBinary [ $impl, R, Wlp [ S, p ] ];
IF x =
NIL
THEN
q ← PUnary [ $all, PBinary [ colon, x, impl ] ]
};
WlpDo:
PRIVATE PROCEDURE [ s : ParseTree, p : Predicate ] RETURNS [ F1 : Predicate ] =
{
-- Wlp ( do I inv G1 => S1 || ... Gn => Sn od, P ) =
I and all u : I impl ((P and not OR(i) Ri) or AND(i) (Ri => Wlp(Si,I)))
1 2 3 4 5 6 7 8 9 10
where
OR(i) Ri means (R1 or R2 or ... Rn)
AND(i) R1 means (R1 and R2 and ... Rn)
u is the list of free variables of the loop that are assigned to (in the loop).
and the numbers under the operators indicate which formula is which. (That is, F1 is (I and F2), F2 is (all F3), and so on.)
If u is empty, return
I and ((P and not OR(i) Ri) or AND(i) (Ri => Wlp(Si,I)))
1 5 6 7 8 9 10
F2, F3, F4, F5, F6, F7, F8, F9 : Predicate;
u : Term; -- the free variables of s that are assigned to in s.
inv : ParseTree ← InvOfDo [ s ];
gcs : ParseTree ← GcmdsOfDo [ s ];
[ F7, F9 ] ← WlpDoGcmds [ gcs, inv ];
F6 ← PUnary [ not, F7 ];
F5 ← PBinary [ $and, p, F6 ];
F8 ← PBinary [ $or, F5, F9 ];
IF ( u ← FreeAsgVars [ s ] ) =
NIL
THEN
F1 ← PBinary [ $and, inv, F8 ]
ELSE
{
F4 ← PBinary [ $impl, inv, F8 ];
F3 ← PBinary [ colon, u, F4 ];
F2 ← PUnary [ $all, F3 ];
F1 ← PBinary [ $and, inv, F2 ]
};
};
WlpDoGcmds:
PRIVATE PROCEDURE [ gcs : ParseTree, inv : Predicate ] RETURNS [ F7, F9 : Predicate ] =
{
-- Calculate formulas F7 and F9 as defined in WlpDo.
moreThanOne : BOOL; -- TRUE if there is more than one guard in the list.
x, R, S : ParseTree; -- the current guard, broken into its parts, x : R => S.
IF gcs = NIL THEN RETURN [ F7 : $false, F9 : $true ];
IF ( moreThanOne ← ( Optr [ gcs ] = box ) ) THEN
{
[ F7, F9 ] ← WlpDoGcmds [ Arg2 [ gcs ], inv ];
[ x, R, S ] ← SplitGcmd [ Arg1 [ gcs ] ];
F7 ← Binary [ $or, Parenthesize [ R ], F7 ];
F9 ← PBinary [ $and, PBinary [ $impl, R, Wlp [ S, inv ] ], F9 ]
}
ELSE
{
[ x, R, S ] ← SplitGcmd [ gcs ];
F7 ← Parenthesize [ R ];
F9 ← Parenthesize [ PBinary [ $impl, R, Wlp [ S, inv ] ] ]
};
};
FreeAsgVars:
PRIVATE PROCEDURE [ s : Stmt ] RETURNS [ v : ParseTree ] =
{
-- We return the free variables of s that are assigned to (in s).
IF s = NIL THEN RETURN [ NIL ];
SELECT Optr [ s ]
FROM
asgn => v ← VarOfAsgn [ s ];
semicolon => v ← Add [ FreeAsgVars [ Arg1 [ s ] ], FreeAsgVars [ Arg2 [ s ] ] ];
$if => v ← FreeAsgVarsOfGcmds [ GcmdsOfIf [ s ] ];
$do => v ← FreeAsgVarsOfGcmds [ GcmdsOfDo [ s ] ];
ENDCASE => ERROR;
};
FreeAsgVarsOfGcmds:
PRIVATE PROCEDURE [ gcs : ParseTree ] RETURNS [ v : Term ] =
{
-- We return an identifier list containing the free variables of gcs that are assigned to in gcs, where gcs is a list of guarded commands, G1 => S1 || ... Gn => Sn.
moreThanOne : BOOL; -- TRUE if there is more than one guard in the list.
IF gcs = NIL THEN RETURN [ NIL ];
IF ( moreThanOne ← ( Optr [ gcs ] = box ) )
THEN
v ← Add
[ FreeAsgVarsOfGcmd [ Arg1 [ gcs ] ]
, FreeAsgVarsOfGcmds [ Arg2 [ gcs ] ]
]
ELSE
v ← FreeAsgVarsOfGcmd [ gcs ]
};
FreeAsgVarsOfGcmd:
PRIVATE PROCEDURE [ gc : Stmt ] RETURNS [ v : Term ] =
{
-- The guarded command gc has of the form G => S. If G is a predicate R then fav(gc) is fav(s). If G is a binding x : R, then fav(gc) = fav(s) minus the variables x.
x, R, S : ParseTree;
IF gc = NIL OR Optr [ gc ] # arrow THEN ERROR;
[ x, R, S ] ← SplitGcmd [ gc ];
IF x =
NIL
THEN
v ← FreeAsgVars [ S ]
ELSE
v ← Subtract [ FreeAsgVars [ S ], x ];
};
Add:
PRIVATE PROCEDURE [ x, y : Term ] RETURNS [ z : Term ] =
{
-- Add together the two identifier lists x and y. Eliminate duplications.
IF x = NIL THEN RETURN [ y ];
IF y = NIL THEN RETURN [ x ];
WITH x SELECT FROM a : ATOM => RETURN [ AddVar [ a, y ] ] ENDCASE;
IF Optr [ x ] # comma THEN ERROR;
z ← AddVar [ NARROW [ Arg1 [ x ], ATOM ], Add [ Arg2 [ x ], y ] ]
};
AddVar:
PRIVATE PROCEDURE [ v : ATOM, y : Term ] RETURNS [ t : Term ] =
{
-- Add the variable v to the term y = var1,var2,...varN.
a : ATOM; -- the first variable of y.
IF y = NIL THEN RETURN [ v ];
WITH y
SELECT
FROM
a : ATOM => RETURN [ IF a = v THEN a ELSE CommaTogether [ v, a ] ]
ENDCASE;
IF Optr [ y ] # comma THEN ERROR;
IF v = ( a ←
NARROW [ Arg1 [ y ],
ATOM ] )
THEN
t ← y
ELSE
t ← CommaTogether [ a, AddVar [ v, Arg2 [ y ] ] ]
};
Subtract:
PRIVATE PROCEDURE [ x, y : Term ] RETURNS [ z : Term ] =
{
-- Take x and subtract off the identifiers of y, where both x and y are identifier lists.
IF x = NIL THEN RETURN [ NIL ];
IF y = NIL THEN RETURN [ x ];
WITH y SELECT FROM a : ATOM => RETURN [ SubtractVar [ a, x ] ] ENDCASE;
IF Optr [ y ] # comma THEN ERROR;
z ← SubtractVar [ NARROW [ Arg1 [ y], ATOM ], Subtract [ x, Arg2 [ y ] ] ]
};
SubtractVar:
PRIVATE PROCEDURE [ v : ATOM, y : Term ] RETURNS [ t : Term ] =
{
-- Remove the variable v from the term y = var1,var2,...varN.
a : ATOM; -- the first variable of y.
IF y = NIL THEN RETURN [ NIL ];
WITH y SELECT FROM a : ATOM => RETURN [ IF a = v THEN NIL ELSE a ] ENDCASE;
IF Optr [ y ] # comma THEN ERROR;
IF v = ( a ←
NARROW [ Arg1 [ y ],
ATOM ] )
THEN
t ← Arg2 [ y ]
ELSE
t ← CommaTogether [ a, SubtractVar [ v, Arg2 [ y ] ] ]
};
CommaTogether:
PRIVATE PROCEDURE [ v : ATOM, y : Term ] RETURNS [ t : Term ] =
{
-- If y is nonNIL, we return (v,y) otherwise we return v.
t ← IF y = NIL THEN v ELSE Binary [ comma, v, y ]
};
-- Tree building routines: build binary and unary trees (with and without parenthesizing the arguments), parenthesize a tree.
PBinary:
PRIVATE PROCEDURE [ op : ATOM, lhs, rhs : ParseTree ] RETURNS [ t : ParseTree ] =
{
RETURN
[ CONS [ op, CONS [ Parenthesize [ lhs ], CONS [ Parenthesize [ rhs ], NIL ] ] ] ]
};
PUnary:
PRIVATE PROCEDURE [ op : ATOM, opnd : ParseTree ] RETURNS [ t : ParseTree ] =
{
RETURN [ CONS [ op, CONS [ Parenthesize [ opnd ], NIL ] ] ]
};
Binary:
PRIVATE PROCEDURE [ op : ATOM, lhs, rhs : ParseTree ] RETURNS [ t : ParseTree ] =
{
RETURN [ CONS [ op, CONS [ lhs, CONS [ rhs, NIL ] ] ] ]
};
Unary:
PRIVATE PROCEDURE [ op : ATOM, opnd : ParseTree ] RETURNS [ t : ParseTree ] =
{
RETURN [ CONS [ op, CONS [ opnd, NIL ] ] ]
};
Parenthesize:
PRIVATE PROCEDURE [ p : ParseTree ] RETURNS [ q : ParseTree ] =
{
IF NotLeaf [ p ] AND Optr [ p ] = lparen THEN RETURN [ p ];
RETURN [ Unary [ lparen, p ] ]
};
-- Selector routines: get various args of a tree.
ArgsOf:
PRIVATE PROCEDURE [ p : ParseTree ] RETURNS [ ParseTree, ParseTree ] =
{
RETURN [ Arg1 [ p ], Arg2 [ p ] ]
};
Optr: PROC [ r : ParseTree ] RETURNS [ a : ATOM ] = { a ← NARROW [ Car[r] ] };
Arg1: PROC [ r : ParseTree ] RETURNS [ ParseTree ] = Cadr;
Arg2: PROC [ r : ParseTree ] RETURNS [ ParseTree ] = Caddr;
SplitGcmd: PROC [ gc : Stmt ] RETURNS [ x, R, S : ParseTree ← NIL ] =
{
-- Split up the guarded command, x : R => S or R => S. (Return x = NIL in the latter case.)
G : ParseTree; -- x : R or R, as appropriate
[ G, S ] ← ArgsOf [ gc ];
IF NotLeaf [
G ]
AND Optr [
G ] = colon
THEN
[ x, R ] ← ArgsOf [ G ]
};
VarOfAsgn: PROC [ p : ParseTree ] RETURNS [ v : ParseTree ] =
{
v ← Arg1 [ p ] -- The variables of an assignment
};
GcmdsOfIf: PROC [ p : ParseTree ] RETURNS [ q : ParseTree ] =
{
q ← Arg1 [ p ] -- the guarded commands of if G => S ... fi
};
GcmdsOfDo: PROC [ p : ParseTree ] RETURNS [ q : ParseTree ] =
{
q ← Arg2 [ Arg1 [ p ] ] -- the guarded commands of do I inv G => S ... od
};
InvOfDo: PROC [ p : ParseTree ] RETURNS [ q : ParseTree ] =
{
q ← Arg1 [ Arg1 [ p ] ] -- the invariant of do I inv G => S ... od
};
Car: PROC [r: ParseTree] RETURNS [ParseTree] = {RETURN[NARROW[NARROW[r, List].first]]};
Cdr: PROC [r: ParseTree] RETURNS [ParseTree] = {RETURN[NARROW[r, List].rest]};
Cadr: PROC [r: ParseTree] RETURNS [ParseTree] = {RETURN[Car[Cdr[r]]]};
Cddr: PROC [r: ParseTree] RETURNS [ParseTree] = {RETURN[Cdr[Cdr[r]]]};
Caddr: PROC [r: ParseTree] RETURNS [ParseTree] = {RETURN[Car[Cdr[Cdr[r]]]]};
-- Inspection routines: check for nonleaves.
NotLeaf: PROC [ p : ParseTree ] RETURNS [ b : BOOL ] =
{
RETURN [ p # NIL AND ISTYPE [ p, List ] ]
};
-- Some testing routines; not normally used otherwise.
Unparse:
PRIVATE PROCEDURE [ p : ParseTree ] RETURNS [ r : ROPE ] =
{
r ← Unparser.Unparse
[ f : CONS [ p, NIL ], culprit : NIL, margin : 60, p : NIL, openCount : 0 ]
};
END.