<<-- TypeCheck.mesa -- last edited by: Jim Sasaki on August 20, 1983 1:05 pm>> <<>> <<-- We calculate the weakest liberal precondition (wlp) of a statement and a predicate. >> DIRECTORY Atom, Rope, Unparser; TypeCheck: DEFINITIONS IMPORTS Atom = BEGIN ROPE : TYPE = Rope.ROPE; -- Short name for Ropes. List : TYPE = LIST OF REF ANY; -- Short name for LIST OF REF ANY Term, Stmt, Predicate, ParseTree, ParseTreeList : TYPE = REF ANY; <<-- abstract syntax trees stored in a lisp-like way.>> Wlp: PUBLIC PROCEDURE [ s : Stmt, p : Predicate ] RETURNS [ q : Predicate ]; END.