SourceForge.net LogoThe Eiffel Compiler / Interpreter (tecomp)

doc/internals/verify eiffel sw/how to prove sw

how to prove sw

What does it mean to prove a routine?

A routine can only be proved, if it has a specification. A routine without specification is always correct with respect to its specification (because it does not have any, although it can still throw exceptions e.g. division by zero, i.e. not meet the preconditions of the called routines).

In Eiffel we have preconditions, postconditions and class invariants to specify the effect of a routine.

Each creation procedure cp has to

at the end. In order to prove a creation procedure we have to prove the class invariant and the postcondition of the procedure at the end. We can assume, that the creation procedure's precondition is valid at its start. It is the obligation of the caller to establish the precondition.

Any other routine can assume that at its start

are valid. It is the obligation of the caller to establish the precondition. It is the obligation of the routine to establish

at the end. Since all routines have to establish the class invariant at the end, the routines can assume it to be valid at the entry point.

Queries

Eiffel has the guideline to adhere to the command query separation. This requirement is not enforced by the language definition. But in order to be able to prove SW it is crucial for queries to not have visible side effects (Asking a question must not change the answer).

But what is a visible sideeffect?

Result creation

A query can return a reference type and create the object during its execution. This by itself is not yet a violation of the purity requirement. The crucial requirement is

  exp ~ exp
 

This is e.g. violated by

   q: TUPLE[r:RT]
      do
         Result := [create {RT}]
      end
 

because two tuples t1 and t2 of type TUPLE[r:RT] are equal, if they contain a reference to the same object.

The problem is caused by a double (or multiple) creation. The result is created by the manifest tuple (which is an implicit creation) and one of the attributes of the created object is created newly as well. If multiple creation happens, the outer created object must have a redefined feature is_equal in order to guarantee the purity requirement exp ~ exp.

Summary: An object creation is a side effect. It is considered harmless, if the purity requirement exp ~ exp is fulfilled.

Caching results

Sometimes queries require significant calculations. If the query is called several times with the same arguments, recalculation is not very effective. In that case it is better to calculate the result only once an put it into a cache attribute. In the subsequent calls only the cached result is returned instead of the recalculation.

Caching results is considered as harmless and is not a violation of the purity requirement.

All attributes changed by queries must be invisible: i.e. the result of no query depends on the invisible attributes.

How to verify that queries do change only invisible attributes?

The verification is done by a fixpoint algorithm:

An example:

class 
  C
feature
     q(arg:A): RT
	 do
	   if not has_cached or else arg /~ arg_cached then
              has_cached := True
	      arg_cached := arg
	      res_cached := q_calculated(arg)
	   end
	   Result := res_cached
         ensure
           Result ~ q_calculated(arg)
	 end
 
feature {NONE}
     has_cached: BOOLEAN
     arg_cached: A
     res_cached: RT
 
     q_calculated(arg:A): RT  
        do
           -- This is the query which does the side effect free calculation
	end
 
invariant
     has_cached implies res_cached ~ q_calculated(arg_cached)
end
 

The query q does have a side effect because it assigns new values to the attributes res_cached and arg_cached. However it always returns the same result as q_calculated would return. So the assignment does not change the value it returns.

It is important that the cached attributes do not change the result of any other query.

If the cached attributes do not change the result of any query, the side effect is not considered as a violation of the purity requirement.

In many cases there is more than one query which wants to use the cached value and/or argument. The it is usually possible to have some kind of cursor and have a side effect free query which calculates the cursor.

  class 
      MAP[KEY,VALUE]
  feature
      has(k:KEY): BOOLEAN
         do
            if is_valid(cursor) implies key_at(cursor) /~ k then
               cursor := cursor_of(k)
            end
            Result := is_valid(cursor)
         ensure
            Result = is_valid(cursor_of(k))
         end
      item alias "[]" (k: KEY): VALUE
         require
            has(k)   -- is_valid(cursor_of(k))
         do
            if is_valid(cursor) implies key_at(cursor) /~ k then
               cursor := cursor_of(k)
            end
            check is_valid(cursor); key_at(cursor) ~ k  end
            Result := value_at(cursor)
         ensure
            Result = value_at(cursor_of(k))
         end
  feature {NONE}
      cursor: INTEGER
      is_cursor(i:INTEGER): BOOLEAN  do ... end
      is_valid (i:INTEGER): BOOLEAN  do ... end
      cursor_of(k:KEY):     INTEGER  do ... end
      key_at(i:INTEGER):    KEY      do ... end
      value_at(i:INTEGER):  VALUE    do ... end
 
  invariant
     is_cursor(cursor)
     is_valid(cursor) implies item(key_at(cursor)) = value_at(cursor)
  end
 

In many cases there is more than one query which wants to use the cached value. Then the update of the cached can be factored out into a side effect free (externally no side effect visible) procedure. Consider

  class 
      MAP[KEY,V]
  feature
      has(k: KEY): BOOLEAN 
         do
           update_cache(k)
           Result := arg_cached ~ k
         end
 
      item alias "[]" (k: KEY): V
         require
            has(k)
         do
           update_cache(k)
           Result := val_cached
         end
 
  feature {NONE}
      update_cache(k: KEY)
         local
            failed: BOOLEAN
         do
            if not failed and (has_cached implies k /~ key_cached) then
               val_cached := item_calculated(k)
               key_cached := k
               has_cached := True
            end
         rescue
            failed := True
            retry
         end
      item_calculated(k: KEY): V
           -- calculate value associated with `k' or throw an exception
         do
           ...
         end
 
      has_cached: BOOLEAN
      key_cached: KEY
      val_cached: V
 
  invariant
     has_cached implies val_cached ~ item_calculated(key_cached)
  end
 

Commands

Queries shall not change the state. Commands do change the state.

Assignment command

The simplest state changing command is the assignment command.

   check 
      domain(exp)  -- preconditions of exp valid
      a(x/exp)     -- all x substituted by exp in a
   end   
 
   x := exp
 
   check 
       a
   end
 

In order to prove that assertion a is valid after the execution of x:=exp we have to prove that domain(exp) and a(x/exp) are valid before its execution.

If assertion a does not contain the variable x, then a(x/exp) = a. I.e. the assignment x:=exp does not have any effect on the validity of the assertion a. Consequence: a has to be valid before the assignment statement.

Calling a command

A command call is usually state changing.

     t.cmd(a)           -- command call
     check
        res
     end
 
 
     class T feature
        cmd(arg: A)
           require
             pre
           do
             ...
           ensure
             post
           end
        ...
      invariant
         inv
      end
 

The command t.cmd(a) can change the state of all objects reachable by t. The objects reachable by t are the objects attached to t and recursively all objects attached to attributes of t and so on.

The command t.cmd(a) affects the assertion res, if res involves any objects which are affected by t.cmd(a).

Ideally the only object affected by the command is the object attached to t and the object is not attached to any other entity. In this ideal case it is sufficient to check, if res involves the entity t to see whether the command affects the assertion.

If t.cmd(a) affects the assertion res, the assertion must be proved from post and inv. If not, the assertion has to be valid unchanged before the command.

Let us assume that t.cmd(a) affects the assertion.

It is necessary that the postcondition of cmd contains enough information to prove res. E.g. if cmd changes one of two attributes of the object attached to t and the postcondition states only the change of the one attribute but does not say anything about the second one and the second one is used in res, res cannot be proved.

Typical example: t is a sequence and t.cmd(a) appends a as the last element of the sequence. Then it is necessary to state in the postcondition that t contains one element more which is now a and that the other elements are unchanged.

I.e. the more complete the postconditions are the higher is the chance to prove the consequences.

 
     check
       pre(formals/actuals,Current/t)  -- new proof obligation
     end
 
     t.cmd(a)           -- command call
 
     check
        post(formals/actuals,Current/t) -- unqualified calls q substituted by
        inv(Current/t)                  -- t.q
     end
 
     check
        res -- has to be proven from post and inv
     end
 

Summary: If t.cmd(a) affects res then res must be a consequence of post and inv. If not, res has to be true before the command.

 Local Variables: 
 mode: outline
 coding: iso-latin-1
 outline-regexp: "=\\(=\\)*"
 End:
Table of contents

- What does it mean to prove a routine?

- Queries

- Result creation

- Caching results

- Commands

- Assignment command

- Calling a command


ip-location