%------------------------------------------------------------------------------
% Continuations
%
% 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
%------------------------------------------------------------------------------
Cont[V:TYPE+]: THEORY
BEGIN
IMPORTING State[V],
orders@lift_props[State],
scott@partial_function_props[State,State]
s,s1,s2: VAR State
Cont: TYPE+ = LiftPartialFunction[State,State] CONTAINING (LAMBDA s: bottom)
x: VAR V
f: VAR [State->int]
c,c1,c2: VAR Cont
p: VAR pred[State]
sq_le(c1,c2):bool = FORALL (s1,s2): c1(s1) = up(s2) IMPLIES c2(s1) = up(s2)
sq_le_def: LEMMA sq_le(c1,c2) IFF
subset?[[State,State]](graph(c1),graph(c2)) % NN 4.8
partial_order_sq_le: JUDGEMENT sq_le HAS_TYPE (partial_order?[Cont])
IMPORTING orders@directed_orders[Cont],
orders@bounded_order_props[Cont,(sq_le)]
D: VAR set[Cont]
lub_graph: LEMMA empty?(D) OR directed?(sq_le)(D) IMPLIES
least_upper_bound?(from_graph(Union(image(graph,D))),D,sq_le)
sq_le_dcpo: JUDGEMENT
sq_le HAS_TYPE (directed_complete_partial_order?[Cont])
sq_le_pdcpo: JUDGEMENT
sq_le HAS_TYPE (pointed_directed_complete_partial_order?[Cont])
sq_le_bottom: LEMMA sq_le((LAMBDA s: bottom),c)
sq_le_least: LEMMA least?(fullset[Cont],sq_le)(LAMBDA s: bottom)
conditional(p,c1,c2):Cont
= (LAMBDA s: IF p(s) THEN c1(s) ELSE c2(s) ENDIF)
sq_le_conditional: LEMMA sq_le(c,conditional(p,c1,c2)) IFF
(FORALL s1,s2: ( p(s1) AND c(s1) = up(s2) IMPLIES c1(s1) = up(s2)) AND
(NOT p(s1) AND c(s1) = up(s2) IMPLIES c2(s1) = up(s2)))
assign(x,f):Cont = (LAMBDA s: up(assign(x,f)(s)))
IMPORTING scott@scott_continuity[Cont,Cont,(sq_le),(sq_le)]
apply_continuous: LEMMA scott_continuous?(LAMBDA c: c o c1)
END Cont
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.19Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
