This is a short manual for the proof of concept implementation of the soundness prover of [vW08]. You can find its web interface here. Please note that this is an experimental tool and as such does not guarantee anything. Of course, questions and comments are welcome.
The soundness prover uses a very basic syntax. See section Examples below for an illustration.
Identifiers | Any alphanumerical string (including underscores) that is not a keyword (i.e. not one of false, true, semantics, relation, axioms, exists or forall). |
Terms are made from variables and function applications:
Variables | Just an identifier. For example, x, x2, f, 0 are all variables. |
Function applications | An identifier followed by zero or more comma-separated terms enclosed by parentheses. For example, f(x), c(), 0(), f(c(),g(x)) are all function applications. |
Formulas:
Boolean constants | false and true |
Predicates | Same as function application; the head symbol is considered the predicate (e.g. P(x)) |
Negation | !f, where f is a formula |
Disjunction | f || g, where f and g are formulas |
Conjunction | f && g, where f and g are formulas |
Implication | f -> g, where f and g are formulas |
Biimplication | f <-> g, where f and g are formulas |
Existential Quantification | <exists x,y,... : f>, where f is a formula and x, y etc are variables |
Universal Quantification | <forall x,y,... : f>, where f is a formula and x, y etc are variables |
Parentheses | (f), where f is a formula |
In text boxes (i.e. Semantics and Auxiliary equalities we also allow comments. These are started with # and are ended by the end of the line in which they are used. Comments are ignored by the parser.
The semantics as given in the Semantics box should consist of the following two non-empty sections.
First the Structural Operational Semantics should be given. This section is started with the keyword semantics and should be followed by one or more SOS rules. A SOS rule is of the form f => p;, where f is a formula and p a predicate. Note the semicolon as last character.
Following the semantics section one needs to define the relation. This is done by writing relation(x,y) where x and y are variables. This is followed by one or more conjuncts that define the relation. Each conjunct is a formula followed by a semicolon (;). In these conjuncts free variables different from those as specified after relation are considered universally quantified. In defining the relation one can use the special predicate rel (with arity 2) to refer to the relation itself.
Inequalities are of the form t <= u or f => t <= u, where t and u are terms and f is a formula. The latter form is called a conditional inequality. Equalities are similar but use an = instead of an <=.
An inequality t < u is interpreted as the claim that rel(t,u) holds and an equality t = u is interpreted as the claim rel(t,u) && rel(u,t). When using a conditional (in)equality the claim is prepend with f ->.
Take the following specification for BPA* [Fok94]:
semantics # act true => tick(act(a),a); # alt tick(p,a) => tick(alt(p,q),a); tick(p,a) => tick(alt(q,p),a); trans(p,a,p2) => trans(alt(p,q),a,p2); trans(p,a,p2) => trans(alt(q,p),a,p2); # seq tick(p,a) => trans(seq(p,q),a,q); trans(p,a,p2) => trans(seq(p,q),a,seq(p2,q)); # star tick(p,a) => trans(star(p,q),a,star(p,q)); trans(p,a,p2) => trans(star(p,q),a,seq(p2,star(p,q))); tick(q,a) => tick(star(p,q),a); trans(q,a,q2) => trans(star(p,q),a,q2); # plus tick(p,a) => trans(plus(p,q),a,alt(plus(p,q),q)); trans(p,a,p2) => trans(plus(p,q),a,seq(p2,alt(plus(p,q),q))); relation(x,y) rel(y,x); trans(x,a,x2) -> <exists y2: trans(y,a,y2) && rel(x2,y2)>; tick(x,a) -> tick(y,a);Copy and paste this in the Semantics box. We will try to prove axioms A1 and BKS2.
In the Axiom box, type alt(x,y) = alt(y,x) and click on Prove it! This should return True, as one would except. Do note, however, that to prove this axiom, one needs reflexivity (x <= x) as well. By default this inequality is added as auxiliary inequality. You can turn this of by unchecking the add reflexivity box. (Try it and see what happens.)
Now lets take a more complex axiom. Enter seq(star(x,y),z) = star(x,seq(y,z)) in the Axiom box. This is axioms BKS2 ((x*y).z = x*(y.z)). When you click on Prove it! you will notice that it takes a while before a result is returned. This is often the case when equalities cannot be proven sound by the prover.
The output should be similar to the following:
False might need "@APPL@"("@R@"(),"seq"("seq"("p20","star"("p","q0")),"q"),"seq"("p20","star"("p","seq"("q0","q")))) (in context "trans"("p","a","p20")) error: timeoutIt states that could not find a prove within the given time limit. However, it also suggest that the reason for this is that it might need an auxiliary equality. Translated, it says that it thinks it needs the inequality seq(seq(p20,star(p,q0)),q) <= seq(p20,star(p,seq(q0,q))) (or x.(y*z).v <= x.(y*(z.v))). It also gives some context information. In this case we also have that p can do a transition to p20. We do not need this information in this case.
Now take the advice of the prover and add the equality seq(seq(p20,star(p,q0)),q) = seq(p20,star(p,seq(q0,q))) to the Auxiliary equalities box. Do not forget to append a semicolon (;) to it (see Syntax above). Clicking on Prove it! will now result in a positive answer.
Fok94 | W. Fokkink, Clocks, Trees and Stars in Process Theory. PhD. thesis, University of Amsterdam, 1994. |
vW08 | M. van Weerdenburg, Automating Soundness Proofs. SOS 2008, to appear. |