This page documents the KIV formalization of
Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Stefan Bodenmüller, Wolfgang Reif:
Symbolic Execution of a Clash-Free Subset of ASMs.
Submitted to Science of Computer Programming Special Issue: ABZ 2017.
The earlier version for the ABZ conference 2016 can be found here. Note that the clash-freedom check is now called cfc(R) in the journal paper, while the KIV specification still uses con(R).
Theorem 1 (Correctness of dep) If A and A' agree on all locations in Dep(R,f)Aξ then the sets Asg(R,f)Aξ and Asg(R,f)A'ξ are equal.
Theorem 2 (Correctness of asg) If (f,a,b) ∈ U for some a, b then A,ξ{x ↦ a} ⊧ asg(R,f,x).
Theorem 3 (Sequential Rules are consistent) If R is sequential (seq(R) holds), then A,ξ ⊧ con(R).
Theorem 4 (Correctness of con) If A,ξ ⊧ con(R) then U is consistent.
Theorem 5. Given a rule R with mod(R) = f and assuming a clash-free rule,
then ⟦R⟧(A,ξ) ▷ U implies that A ∪ (A⊕U)' ⊧ rel(R)(f,f').
The weaker theorems that assumed A,ξ ⊧ con(R) (instead of clash-freedom) can be found here and here.
You are invited to skip directly to clash-freedom check or to the relational semantics.
x,y: variablef,g,h: functiona,b: value with a constant _trueu: update, where a concrete update _(f,a,b) is written with a leading underscore.A term t: term is either a variable (embedded as ⌜x⌝) or application of a function to an argument (written f[t]).
ASM rules R: rule comprise
f[t1] := t2, written _asg(f,t1,t2)_par(R1,R2) and sequential _seq(R1,R2) composition_if(t,R1,R2)_call(ρ, t, h, u); they have a single value and a single reference parameter hereTo support recursive calls, the semantics of rules is defined using a fixpoint of the imported Knaster-Tarski fixpoint theory.
Rule declarations are abstractly given by two functions ρ.x and ρ.R(f, x). The first function returns the formal value parameter, while the second returns the procedure body where the formal reference parameter has been replaced with f(x). Note that the uninstantiated body and the formal reference parameter are not explicitly specified, avoiding the need to specify substitution in rules.
The semantics is given in terms of
ξ: variable → valueA: function × value → value, where the carrier set is implicitly given by the type value (including the booleans with a constant _true)U: update → bool are modeled as higher-order function variables for convenience.Modification of a valuation at variable x to a new value a is just function override, written ξ(x;a) in KIV, similarly for algebras.
The semantics ⟦t⟧(A,ξ) of terms t is standard.
The update semantics ⟦R⟧>(A,ξ)(U) of rules R denotes whether R yields the set of updates U. It is defined recursively over the structure of rules (axioms sem-*). The cases are straight forward transcription of the inductive system given e.g. by Börger 1 or Stärk and Nanchen 2, except that true nondeterminism is used here instead of choice functions, i.e., several U may satisfy ⟦R⟧>(A,ξ)(U). We point out some specific aspects of the encoding:
_asg(f,t1,t2) is a predicate λ u. u = _(f, ⟦t0⟧(A,ξ), ⟦t1⟧(A,ξ)) characterizing this one update u.R1 and R2takes apart two cases, depending on whether the first update set U1 is consistent (predicate con(U1)). The second rule then starts in a modified algebra A ⊕ U1.(φ ⊃ a ; b) as in the paper.a such that the test t evaluates to the (semantic) constant _true. The body is then executed with the modified valuation ξ(x;a).aU: value → (update → bool)a that is either computed by the body or forced to be empty when the test does not hold.U is then the union of all these aU(a) (operator U_ .). Admittedly, the notation is a bit overloaded here.Several helper lemmas about the relation of algebras and update sets are proved here.
The function symbols and variables occuring in terms and formulas are defined here.
The specifications dep-sem and asg-sem first characterize the semantic sets Dep and Asg of the paper via predicates ∈dep and ∈asg. All main theorems are proved on this basis. We prove equivalence to their syntactic counterparts defined in dep-asg as theorems dep-has-sem and asg-has-sem. Compared the proofs for the conference version (see here) this has the advantage of keeping the main proofs separate from proofs of coincidence lemmas, e.g. asg-coincidence and asg-var-swap.
The predicate ==(R, f, ξ)(A, A') means that A and A' agree on all locations in Dep(R,f)Aξ. It implies (see theorem dep-theorem or Lemma 6 of the paper) that the two dependency sets Dep(R,f)Aξ and Dep(R,f)A'ξ are equal. The latter is abbreviated as predicate =dep(R, f, ξ)(A, A') (see its definition). Similarly, the predicate =asg(R, f, ξ)(A, A') (see its definition) is true, iff the f-locations in Asg(R)Aξ and Asg(R)A'ξ are the same.
dep) proves a coincidence for Asg. It depends on a similar coincidence for terms to show that the conditions of conditionals and choose/forall match up.The set of functions f modified by R is is characterized by mod(R,f). The dependencies g(y) that possibly affect arguments of f in R is given by predicate dep(R,g,y,f). Whether function f is possibly assigned for an argument x in the algebra A and valuation ξ is characterized by asg(R,f,x)(A,ξ). The only complex case is that for sequential composition.
For asg and con, we have taken a shallow approach to the embedding (in contrast to the embedding for rules): In the paper, these generate syntactic formulas that can be checked by an external tool. Here, we refrain from a deep encoding of formula syntax as a data type. Since we only ever need the evaluated forms, i.e., A,ξ ⊧ asg(R,f,x) and A,ξ ⊧ con(R) in the notation of the paper, we directly give the result of evaluating the respective formula over A and ξ.
Clash-freedom check is given by con(R)(A,ξ). Sequential composition quantifies the algebra A instead of renaming the modified function symbols in the second rule R2. The values of functions g ∉ mod(R1) are kept, others are discarded, reflecting the freshness condition on such functions.
The proofs for the lemmas and theorems are all by induction over the structure of the rule.
Theorem 2 (Correctness of asg) encodes the assumption that the designated z from the paper do not occur otherwise as an assumption ¬ x ∈ R (as defined here). The interesting case is sequential composition, which depends on the correctness of mod and dep to establish that f has not been affected by the first part of the sequential composition.
Theorem 3 (Sequential Rules are consistent) is easy to prove.
Theorem 4 (Correctness of con) needs some manual interaction (hollow proof nodes) for instantiating the hypotheses, in particular, the proof for the forall construct is somewhat tedious, because updates of different runs of the body have to be compared.
The relational encoding rel(R)(A,A0,ξ) relates two algebras A and A0, where A stores the unprimed function symbols f and A0 stores their primed counterparts. Similarly to the formalization of asg and dep, the semantics is thus intertwined with the definitions to spare us to reason about syntactic renaming (the additional overhead seems not justified as the main results are reflected faithfully anyway).
The merge operation for parallel composition is thus done on the level of algebras A1 and A2 resulting from the respective subrule.
The forall construct is encoded in terms of a mapping Af that gives the resulting algebra for the run of the body R for index a like it has been done for the update semantics.
The calculus defines the wlp-operator (box) here. It proves that for a consistent rules it can be expanded to the relational encoding. It also proves the soundness of the forall rule.