Soundness Prover

Introduction

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.

Syntax

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.

Semantics

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.

(In)equalities

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 ->.

Example

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);

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: timeout

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.

References