Quelle  BExp.pvs

%------------------------------------------------------------------------------
% Boolean Expressions
%
% All references are to HR and F Nielson "Semantics with Applications:
% A Formal Introduction", John Wiley & Sons, 1992. (revised edition
% available: http://www.daimi.au.dk/~hrn )
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
%     Version 1.0            25/12/07  Initial Version
%------------------------------------------------------------------------------

BExp[V:TYPE+]: THEORY

BEGIN

  IMPORTING State[V], AExp[V]

  s:     VAR State

  BExp: DATATYPE  
  BEGIN
    TT               : TT?
    FF               : FF?
    Eq(a1,a2:AExp)   : Eq?
    Le(a1,a2:AExp)   : Le?
    Neg(b:BExp)      : Neg?
    Band(b1,b2:BExp) : Band?
  END BExp

  B(b:BExp) : RECURSIVE [State->bool] =
    LAMBDA s: cases b of
                      TT         : True,
                      FF         : False,
                      Eq(a1,a2)  : A(a1)(s) =  A(a2)(s),
                      Le(a1,a2)  : A(a1)(s) <= A(a2)(s),
                      Neg(b)     : NOT (B(b)(s)),
                      Band(b1,b2): B(b1)(s) AND B(b2)(s)
                    endcases
                    MEASURE b by <<

END BExp