This module provides the abstract representation of PLSEQ programs and specifications. PLSEQ is an abbreviation of Programming Logic for Sequantial programs. It is a very simple logic.The language of PLSEQ consists of the language of programs, which is used to express or write a program, and a specification language which is used to express a specification of a program. The programming language is C-like.
The specification language is a simple Hoare triple language.
Both the programming and specification languages share an expression language. We will used the expression language defined by ExprDD and ExprParser. It is a very rich expression language, and with it we can easily express complicated specifications (think for example a sorting program; the program itself may only use an array, but its specification is complicated).
To be more precise, PLSEQ is actually not a logic for a complete programs. It is a logic of sequentially composed statements. It is intended to be used as a part of a bigger logic, such as PLTEM. PLSEQ has no language construct to form a complete program. Instead, it is assumed that PLSEQ specifications are produces by an external tool that parses a complete program of some other language.
datatype Stmt = Asg of string * Expr | Inc of string | Dec of string | Seq of Stmt list | If of Expr * Stmt * Stmt | Case of (Expr * Stmt) list * Stmt | While of Expr * Expr * Stmt | ForLoop of Expr * string * Expr * Expr * Stmt * Stmt
- Asg (x,e) represents assignment x=e.
- Inc i represents increment statement i++. Conversely Dec i represents i--.
- If (g,s,t) represents an if-then-else statement.
- Case s e represents a case-statement. The s is a list of guard the its corresponding statement. The e is the else part. The else part is compulsory.
- While (i,g,s) represents a while statement. The i is the loop invariant.
- ForLoop (I,i,lb,up,inc,body) represents a for-loop, for example:
The i is called the looping counter. The loop terminates if the value of i at least equal to the loop upper bound, in this case 10.inv I for (i=0; 10; i++) s = s + a[i]A for-loop is restricted in the following way. The loop body should not contain any assignment to this counter, nor any program variable occuring in the loop lower bound (lb) and upper bound (ub). This greatly simplify the termination proof of the loop. We only need to prove that the loop increases the counter.
datatype info SEQSpec = Every of Expr * info | Hoa of Expr * Stmt * Expr * info
info is additional information which may be needed to interpret the specification. For example, it may contain the list of all program variables used, and their typing.