PLSEQDD

DATE : august 2001
AUTHOR : underdarkPrime underdarkPrime@yahoo.com

Index


  1. SEQSpec
  2. Stmt

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.


Stmt

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






SEQSpec

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.


Generated by mosmldoc --underdarkPrime