Changes between Version 16 and Version 17 of ContractReduction

Timestamp:

07/21/14 16:02:43 (12 years ago)

Author:

siegel

Comment:

--

ContractReduction

@@ -77 +77 @@
 Claim: for any process p, if AMPLE(s,p) contains a process with at least one enabled transition in s,
 then it defines an ample set, i.e., from any execution departing from s, no transition dependent
-on a transition from a proc in AMPLE(s,p) can occur without a transition from a proc in AMPLE(s,p) occurring first.
+on a transition from a proc in AMPLE(s,p) can occur without a transition from a proc in
+AMPLE(s,p) occurring first.
 
-Proof:  Let AMPLE=AMPLE(s,p).
+=== Proof of Claim ===
+
+Let AMPLE=AMPLE(s,p).
+
 Let
 
@@ -98 +102 @@
 from a proc in A(s,S0,q0) occurring first.  Hence for some i, t_i is from a proc in A(s,S0,q0), and therefore t_i is in AMPLE,
 contradicting the ASSUMPTION.  QED.
+
+=== Use of `$depends` ===
+
+In the case where S is a function call, the `$depends` clause in the function contract specifies the
+set A(s,S,p) as follows: first the depends clause specifies a predicate d(s,q) where s is a state and
+q is a proc.  Then
+
+A(s,S,p) = {p} U {q|d(s,q)}
+
+