%------------------------------------------------------------------------------
% 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
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.122Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchen
Entwicklung einer Software für die statische Quellcodeanalyse
|
