Proofs made easy with proof procedures

Introduction

The Modern Eiffel project has two major goals: Design and implement a language
which (a) allows formal verification and (b) is usuable by programmers.

The second goal has not yet been fully met, because the interface to the proof
engine is not easy to grasp for prgrammers coming from object oriented
languages like C++, C#, Java, Scala, etc.

This needs to be improved because “Formal methods will never have a
significant impact until they can be used by people who don’t understand
them (attributed to Tom Melham)”.

The automation features of Modern Eiffel’s proof engine (i.e. assertions
without explicit proof are proved by the proof engine with the implicit
command “resolve”) already reduces the need for explicit proofs
significantly.

However not all provable assertions can be proved automatically. In some cases
user intervention is required.

This article describes a user interface to the proof engine which makes it
possible to write the proofs like a procedure. Therefore proving an assertions
will become more like programming (which programmers might like more than
issuing proof commands).

Proof procedures

Normal procedures

We have not yet introduced procedures up to now, because we have not yet
worked with mutable objects.

A procedure in Modern Eiffel looks like any other procedure in other
programming languages except that it has preconditions and postconditions.

  some_procedure(a:A, b:B, ... )
    require
      pre_1; pre_2; ...
    do
      cmd_1; check a;b;c end; cmd_2; cmd_3; ...
    ensure
      post_1; post_2; ...
    end

The preconditions specify which conditions must be valid at the entry
point. It is the caller’s responsibility to satisfy the preconditions and it
is the responsibility of the called procedure to establish the
postconditions. The pre- and postconditions form a contract between the caller
and the called procedure. The contract is the specification of a procedure.

The body is a sequence of commands interleaved with some assertions (i.e. the
“check … end” commands). At the end of the body the postcondition has to be
established.

Proof procedures

Now assume that we want to prove an assertion like

  all(x:X, y:Y)
     a => b => c => check p;q end

  -- this assertion is equivalent to the two assertions
  all(x:X,x:Y) a => b => c => p
  all(x:X,x:Y) a => b => c => q

With a little syntactic sugar we rewrite the assertion as

  all(x:X, y:Y)
    require
      a; b; c
    ensure
      p; q
    end

In this form the assertion already looks like an unnamed procedure without
body.

Note that the preconditions can be empty.

  all(x:X, y:Y) check p;q end

  -- is equivalent to
  all(x:X, y:Y)
    ensure
      p; q
    end

I.e. an assertion can be viewed as a procedure callable with any arguments
satisfying the precondition and ending in a state satisfying the
postcondtion. Since it should be a proof procedure, it must not modify
anything.

The body of a proof procedure is the actual proof. The simplest body of a
proof procedure is just a sequence of assertions.

  all(x:X, y:Y)
    require
      a; b; c
    do
      a1   -- state: a, b, c : a1
      a2   --        a, b, c, a1 : a2
      ...
    ensure
      p   -- state: a, b, c, a1, a2, ... : p
      q   --        a, b, c, a1, a2, ... p : q
    end

A proof procedure is correct if the proof engine can prove all intermediate
assertions and the postconditions by using all previous assertions and the
already proved assertions as assumptions. In the above code snippet the
corresponding start state of the proof engine is added as a comment.

At each intermediate assertion and each postcondition the proof engine enters
the corresponding state and tries to proof the assertions under the
assumptions on the assumption stack and with the help of the already proved
asseritions. If all assertions can be proved automatically, then the proof
procedure is valid.

Example: Commutativity of “and”

In this example we want to prove the commutativity of “and” stated as

  all(a,b:BOOLEAN) a and b => b and a

This assertion can be proved by the proof engine automatically, therefore no
explicit proof is required. But in order to demonstrate the technique we give
a very pedantic proof in form of the following proof procedure.

  all(a,b: BOOLEAN)
    require
      a and b
    do
      elim1: a and b => a
      elim2: a and b => b
      a
      b
      intro: b => a => b and a
    ensure
      b and a
    end

“elim1” and “elim2 are valid, because they have already been proved within the
introduction of the boolean operation “and”.

The next two assertions are immediate consequences of the precondition and
“elim1” or “elim2” respectively.

“intro” is valid; it has already been proved within the “and” operation.

The postcondition is an immediate consequence of “a”, “b” and “intro”.

In order to compare here is a proof with explicit proof commands (at the same
pedantic level).

  all(a,b:BOOLEAN) check
    a and b => b and a
      proof
        enter
        premise(b,a)
        premise(a and b)
        remove
        premise(a and b)
        remove
      end
  end

Example: Exclusion of an alternative

If we have an alternative “a or b” and we know that “a” is false, then “b”
must be true. I.e. we expect the following to be valid.

  all(a,b:BOOLEAN) (a or b) => not a => b

We prove this assertion with the following proof procedure.

  all(a,b:BOOLEAN)
    require
      a or b
    do
      contra:  a => not a => b  -- from a contradiction follows anything
      trivial: b => not a => b

      elim:   all(x:BOOLEAN) 
                (a or b) => (a=>x) => (b=>x) => x
    ensure
      not a => b
    end

The assertions “contra” and “elim” are already proved assertions (just made
more specific than the general laws). The assertion “trivial” is a
triviality. The postcondition is discharged implicitely with the commands

  premise(a or b, a => (not a => b), b => (not a => b)
  remove(3)

The intermediate assertions “contra” and “trivial” are not necessary. They
have been inserted to make some intermediate steps more explicit.

Let us compare the above proof procedure with a proof with proof commands. We
could proof the above assertion like

  all(a,b:BOOLEAN) check
    a or b => not a => b
      proof
        enter
        case_split(a, b)
        remove
        resolve
      end
  end

The proof with proof commands is more compact. The proof procedure is more
verbose. It is a matter of taste which proof one writes. However from the
perspective of programmers the proof by a proof procedure might be
preferable.

Example: Contrapositive

In order to prove the contrapositive law

  all(a,b: BOOLEAN
    (a => b) => (not b => not a)

we can write the proof procedure

  all(a,b: BOOLEAN)
    require
      a => b
      not b
    do
      a1: (a => b) => (a => not b) => not a
    ensure
      not a
    end

The intermediate assertion “a1” matches an already proved assertion. The
postcondition “not a” is proved by entering the state

  a => b
  not b
  (a => b) => (a => not b) => not a
  =================================
  not a

The goal “not a” is discharged automatically by the proof engine with the
commands

  -- proof commands generated by the proof engine
  premise(a => b, a => not b)
  remove
  enter
  remove

The above proof procedure can be improved with respect to readability and
clarity. An alternative form is:

  all(a,b: BOOLEAN)
    require
      a => b
      not b
    do
      require
        a         -- Assume the opposite ...
      ensure
        b; not b  -- and derive a contradiction
      end
    ensure
      not a       -- therefore `not a' must be valid
    end

Proofs belong to the implementation

Since proof procedures are more verbose than proofs by proof commands it is
important to split the specification and the implementation part.

The statement of an assertion belongs to the specification part, the actual
proof to the implementation part.

I.e. in the above example “commutativity” the specification part should
include just

  all(a,b:BOOLEAN) a and b => b and a  

and the implementation part should include the proof procedure

  all(a,b: BOOLEAN)
    require
      a and b
    do
      elim1: a and b => a
      elim2: a and b => b
      a
      b
      intro: b => a => b and a
    ensure
      b and a
    end

This keeps the specification part compact and readable. As described in the
article “Specification and implementation of modules” Modern Eiffel allows
this physical separation of specification and implementation.

Usage of “control flow” in proof procedures

Alternative commands

In Modern Eiffel we have the two versions of an alternative command, the
if-command and the inspect-command. They look like

  if c1 then
    stmt1
  elseif c2 then
    stmt2
  ...
  else
    stmt_else
  end

  inspect 
    e
  case p1 then
    stmt1
  case p2 then
    stmt2
  ...
  end

If one of these alternative commands is embedded within a sequence of
assertions in a proof procedure, then the proof procedure does not have only
one sequence of assertions but n sequences of assertions. Each of these n
sequences must be provable as a linear sequence.

In case of nesting the corresponding sequences multiply correspondingly. Deep
nesting is not recommendable neither in executable nor in proof procedures.

Proof pattern for an if-command

The code snippet below shows the possibilities for a four branch if-command.

  all(x:X, y:Y)
    require
      a; b; c
    do
      ... 
      s

      if c1 then
        a1  -- state: ..., s, c1 : a1
        ...
        e1  -- state: ..., s, c1, a1 : e1
      elseif c2 then
        a2  -- state: ..., s, not c1, c2 : a2
        ...
        e2  --        ..., s, not c1, c2, a2, ... : e2
      elseif c3 then
        a3  -- state: ..., s, not c1, not c2, c3 : a3
        ...
        e3  --        ..., s, not c1, not c2, c3, a3, ... : e3
      else
        a4  -- state: ..., s, not c1, not c2, not c3 : a4
        ...
        e4  --        ..., s, not c1, not c2, not c3, a4, ... : e4
      end

        t  -- states: ...,s, ..., e1 : t
           --         ...,s, ..., e2 : t
           --         ...,s, ..., e3 : t
           --         ...,s, ..., e4 : t
        ... 
    ensure
      p
      q
    end

Example: Commutativity of “or”

The commutativity of “or” can be stated in the specification file like

  all(a,b:BOOLEAN) a or b => b or a

The following proof procedure proves this assertion by using an if-command to
realize the case split.

  all(a,b:BOOLEAN)
    require
      a or b
    do
      if a then
        a; b or a
      else
        proved: (a or b) => not a => b
        not a; b; b or a
      end
    ensure
      b or a
    end

There should be no problem to read and verify this proof procedure.

Recursive proof procedures

Proof procedures do nothing. If called, instead of executing instructions,
they prove the postcondition provided that the precondition is valid.

Since they “do” nothing the question arises “Why not call them
recursively?”. And indeed this is possible, provided that the recursion is
guaranteed to terminate (i.e. at least one argument which is bounded from
below is decreasing).

Suppose we have the module “unary_natural” with the following class and
function definition.

  case class UNARY_NATURAL create
    zero
    succ(pred:UNARY_NATURAL)
  end

  feature
    + (a,b:UNARY_NATURAL): UNARY_NATURAL =
        inspect b
        case zero    then a
        case succ(p) then succ(a+p)
        end
  end

The corresponding type UNARY_NATURAL is an inductive type. Therefore recursion
is well behaved.

Suppose we want to prove the assertion:

  all(a:UNARY_NATURAL)  zero + a = a

Let us rewrite the assertion into an equivalent form which looks more like a
procedure.

  all zero_left_neutral(a:UNARY_NATURAL)  
    do
      ...
    ensure
      zero + a = a
    end

We have given the procedure a name. The name is just a local binding within
the proof procedure and does not “pollute” the namespace of the enclosing
module.

The procedure “zero_left_neutral”, if called with any actual argument “arg”
should establish the truth of “zero+arg=arg”. In the following proof procedure
we mimick the recursive definition of “+”. I.e. as the next refinement we get

  all zero_left_neutral(a:UNARY_NATURAL)
    do
      inspect a
      case zero then
        a = zero
        zero+zero=zero 
        zero+a = a
      case succ(p) then
        ...
      end
    ensure
      zero + a = a
    end  

We do a pattern match on the argument. In the case that “a” is zero the proof
is a triviality. All intermediate assertions (spelled out pedantically – which
is not necesary) are direct consequences of the definition of “+” in the case
“a=zero”.

In the case “a=succ(p)” the pattern match instantiates a fresh variable “p”
with a value which is strictly smaller than “a”. Therefore we can call the
procudure “zero_left_neutral” with the argument “p”. This call proves
“zero+p=p”. We can combine this fact with the fact “a=succ(p) and the
definition of “+” and we get the following complete proof procedure.

  all zero_left_neutral(a:UNARY_NATURAL)
    do
      inspect a
      case zero then
        a = zero
        zero+zero=zero 
        zero+a = a
      case succ(p) then
        zero_left_neutral(p)  -- recursive call!
        zero + p = p
        a = succ(p)
        succ(zero+p) = succ(p)
        zero + a = a
      end
    ensure
      zero + a = a
    end

This proof procedure is very detailed. Since many steps are trivial, we can
let the proof engine do them automatically. A more compact version of the
above proof reads like

  all zero_left_neutral(a:UNARY_NATURAL)
    do
      inspect a
      case zero then          -- trivial
      case succ(p) then
        zero_left_neutral(p)  -- recursive call!
        succ(zero+p) = succ(p)
      end
    ensure
      zero + a = a
    end

Iterative proof procedures

One might be tempted to convert the recursive proof procedure into an
iterative one. Using a loop we can construct the truth of “zero+a=a”
bottoms up. We write a loop with a variable “i” which is initialized to zero.

The loop should maintain the invariant “zero+i=i”. The loop advances by
incrementing “i” each iteration by one until it reaches the value of “a”. At
the loop termination the truth of “zero+a=a” is established.

The proof procedure looks like:

  all(a:UNARY_NATURAL)
    local
      i:UNARY_NATURAL
    do
      from      i := zero
      invariant zero<=i; i<=a  
                zero + i = i
      variant   a - i
      until     i = a
      loop
        i < a
        succ(i) <= a
        zero + i = i
        succ(zero+i) = succ(i) 
        zero+succ(i) = succ(i)

        i := succ(i)
      end
      zero+i=i; i=a
    ensure
      zero + a = a
    end

In order to verify this procedure formally we need the assignment axiom

  check e[x:=exp] end
  x := exp
  check e end

The assignment axiom tells us the following: If we want to establish the
assertion “e” after the assignment “x:=exp”, we have to prove that “e[x:=exp]”
is a valid assertion before the assignment command.

It is not difficult to see that the loop maintains the invariant and decreases
the variant at each iteration.

At termination we have the invariant and the exit condition which together
imply the postcondition.

In my opinion the recursive proof procedure is better readable and
understandable than the iterative. But some might prefer a loop …

Summary

The notion of a proof procedure instead of a proof by proof commands has been
developed in this article.

It seems that proof procedures are a little bit more verbose than proofs by
proof commands. But they look more understandable than proof
commands. Furthermore they are closer to the activity which software
developers have to do anyhow: Programming.

In the next articles I will experiment more with proof procedures to get a
better feeling about the advantages and disadvantages of this approach.

Advertisements
  1. #1 by Colin Adams on May 15, 2012 - 6:16 am

    I just discovered this blog today, and read all the articles.

    It’s very interesting, but I assume you DON’T have an implementation yet?

    Also “Modern Eiffel” does not look like a good name for a programming language (just imagine a verbal discussion – the possibility of confusion is obvious). I would suggest “brandl” (all lower case).

    • #2 by helmutbrandl on May 17, 2012 - 11:41 am

      Do you know the programming languages ritchie, gosling, meyer, odersky?

      No? I don’t know them either. I just know C, Java, Eiffel, Scala.

      The language I am proposing is actually a variant of Eiffel. I have called it (as a working title) “Modern Eiffel” because it is a modern version of Eiffel. Many design deficiencies of Eiffel are removed in Modern Eiffel.

      No, there is no implementation yet. If you read the articles you will realize that the language is still evolving. It needs to stabilize more before the implementation.

      What confusion do you see? You have C, C#, C++. Nobody complains about possibly confusion. With Eiffel you have ISE Eiffel, SmartEiffel, Liberty Eiffel and Modern Eiffel. Where is the problem?

  2. #3 by doublecnz on May 17, 2012 - 9:06 pm

    Doing proofs via programming proof procedures seems similar to the ATS approach to proofs. (eg. see http://arxiv.org/abs/1203.6102). Is this the sort of approach you are looking at?

    • #4 by helmutbrandl on May 19, 2012 - 5:29 pm

      I don’t know the ATS approach. Therefore I cannot comment on it.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: