If are some states, is the action of the non-deterministic program on those states, and and then: +
If \(Σ\) are some states, \(⟦C⟧:Σ→ 𝒫(Σ)\) is the action of the non-deterministic program \(C\) on those states, and \(σ,τ : Σ\) and \(P,Q⊆Σ\) then:
Postcondition “over-approximates” , it's allowed to include some unreachable outcomes.
+Postcondition \(Q\) “over-approximates” \(⟦C⟧^\dagger(P)\), it's allowed to include some unreachable outcomes.
Postcondition “under-approximates” , it's allowed to leave out some reachable outcomes
+Postcondition “under-approximates” \(⟦C⟧^\dagger(P)\), it's allowed to leave out some reachable outcomes
Both HL and IL combine two difference sources of outcome multiplicity:
@@ -75,47 +75,47 @@Heisenbugs: “Every state in the precondition can (sometimes, nondeterministically) produce an error”
Correct Shuffles: “Each of several postconditions is (sometimes, nondeterministically) reachable from every state in the precondition”
-Manifest Errors (Le et al.): “Executing on any state terminates erroniously in some state satisfying…”
+Manifest Errors (Le et al.): “Executing \(C\) on any state terminates erroniously in some state satisfying…”
look at properties of the sets for , or actually more generally, for .
-A Heisenbug means that overlaps error, for any choice of .
-
A fair shuffle means that covers your shuffle outcomes, for any choice of .
+look at properties of the sets \(⟦C⟧(x)\) for \(x∈ P\), or actually more generally, \(⟦C⟧^\dagger(X)\) for \(X \subseteq P\).
+A Heisenbug means that \(⟦C⟧^\dagger(X)\) overlaps error, for any choice of \(X\subseteq P\).
+
A fair shuffle means that \(⟦C⟧^\dagger(X)\) covers your shuffle outcomes, for any choice of \(X\subseteq P\).
Because we're interested in properties of - , we need to promote + \(⟦C⟧^\dagger(X)\), we need to promote \(⊨\) from a relation between states and assertions to a relation between sets of states and assertions.
To do this (and get the nondeterministic outcome logic from the paper) we supply:
and we extend satisfaction (skipping classical connectives ):
+ \(φ::= ⊤ \mid ⊥ \mid φ∧ψ \mid φ⇒ψ \mid φ\oplus ψ \mid ⊤^\oplus\mid p\) +and we extend satisfaction (skipping classical connectives \(⊤,⊥,∧, ⇒\)):
| iff | where | +\(S ⊨ φ\oplusψ\) | iff | \( S=T∪R\) where \(T ⊨ φ, R ⊨ ψ\) | |
| iff | + | \(S ⊨ ⊤^\oplus\) | iff | \( S=\varnothing\) | |
Observe:
expresses partial +
\(⟨φ⟩C⟨ψ∨⊤^\oplus⟩\) expresses partial correctness.
Holds just in case given a set of states - satisfying , produces - either a set of states satisfying , or the empty + satisfying \(φ\), \(⟦C⟧^\dagger\) produces + either a set of states satisfying \(ψ\), or the empty set.
expresses under-approximation.
holds just in - case every set of states satisfying - contains some member that sends to - a state contained in .
+\(⟨φ⟩C⟨p\oplus + ⊤⟩\) expresses under-approximation.
holds just in + case every set of states satisfying \(φ\) + contains some member that \(⟦C⟧\) sends to + a state contained in \(v(p)\).
We get a lot of expressive power.
Given a concrete , concrete command language generating - , and concrete atoms , you can +
Given a concrete \(Σ\), concrete command language generating + \(C\), and concrete atoms \(p\), you can equip OL with a sound proof system to reason about the above.
@@ -167,31 +167,31 @@
Corollary to big theorem:
Nondeterministic OL can falsify HL triples
-we have just in case for some where is satisfiable,
-Or anyway, this holds if is guaranteed to terminate.
+we have \(\nvDash\{p\}C\{q\}\) just in case for some \(φ⇒p\) where \(φ\) is satisfiable, \(⟨φ⟩C⟨\bar{q}\oplus ⊤⟩\)
+Or anyway, this holds if \(C\) is guaranteed to terminate.
What is ?
-Intuitively,
-But,
+What is \(⟦C⟧^\dagger\)?
+Intuitively, \(⟦C⟧ : Σ → 𝒫(Σ)\)
+But, \(⟦C⟧^\dagger : 𝒫(Σ) → 𝒫(Σ)\)
So you do the obvious thing:
- +\(⟦C⟧^\dagger(X) := \bigcup\{⟦C⟧(x) | x ∈ X\}\)
which is really a completely general construction:
- +\(\mathsf{bind}:𝒫(A)→(A→𝒫(B))→𝒫(B)\)
It turns out that this , along with the singleton constructor for , make a monad.
-It also has a little bit of extra structure: and make a commutative monoid, for any .
+It turns out that this \(\mathsf{bind}\), along with the singleton constructor for \(\mathsf{unit}:A→𝒫(A)\), make \(𝒫\) a monad.
+It also has a little bit of extra structure: \(∪\) and \(\varnothing\) make \(𝒫(X)\) a commutative monoid, for any \(X\).
So, callback to earlier:
-An execution model is a triple , where is a Monad, and are the multiplication and unit providing a (partial, commutative) monoid structure on every +
An execution model is a triple \(⟨M,⬦,\mathbf{1}⟩\), where \(M\) is a Monad, and \(⬦,\mathbf{1}\) are the multiplication and unit providing a (partial, commutative) monoid structure on every \(M(X)\)
Outcome logic can be made parametric on a choice of monad, , monoid structure on each , and clause for
+Outcome logic can be made parametric on a choice of monad, \(M\), monoid structure on each \(M(X)\), and clause for \(⊨p\)
The cash value of that fact is that:
For example, given error states , the error - monad is given by , with - propagating error states, and just the right-hand inclusion. +
For example, given error states \(E\), the error + monad is given by \(\mathsf{Er}_E(X) = E+X\), with + \(\mathsf{bind}_E\) propagating error states, and \(\mathsf{unit}_E\) just the right-hand inclusion.
-has the following nice property: there's a uniform way to - give a monad structure, for - any monad . +
\(\mathsf{Er}_E\) has the following nice property: there's a uniform way to + give \(M \circ \mathsf{Er}_E\) a monad structure, for + any monad \(M\).
- So, if is an execution model, so is . + So, if \(⟨M,⬦,\mathbf{1}⟩\) is an execution model, so is \(⟨M\circ \mathsf{Er}_E,⬦,\mathbf{1}⟩\).
In particular, we get an execution model for non-determinism with errors, which the authors use for non-deterministic separation logic.