Practical Aspects of Imperative Program Verification in Theorema

Kovacs Laura Ildiko, Tudor Jebelean
Research Institute for  Symbolic Computation, Linz
Institute e-Austria Timisoara, Romania
{lkovacs, jebelean}@risc.uni-linz.ac.at

Initializitaion of the system

Loading VCG

Needs["Theorema`Experimental`Verification`VCG`"]

Program Verification

Verification Systems

PVS

SPARKS

DAIKON

The Theorema System

Theorema - a computer aided mathematical assistant for automated reasoning

the 'Theorema Language':  a version of higher order predicate logic (with equalities as rewrite rules)

composing, structuring and manipulating arbitrarily complex mathematical texts consisting of formal mathematical expressions together with structural information like labels, keywords like 'Definition', 'Theorem', etc.

'computing' (simplifying), 'solving', and 'proving' mathematical expressions using specified 'knowledge bases' and applying the various simplifiers, solvers, and provers from the Theorema library.

Program Verification in Theorema

working with: 
	- logical formulae
	- description of algorithms

proofs in natural language (using natural style inferences)

powerful computing and solving algorithms

Program Verification in Theorema

Infrastructure (by Martin Kirchner)

Special Constructs

Program, Specification, Execute

Procedural language

Example: Division of two natural numbers

\(Specification["Division", 
		\ \ \ \ \ \ \ \ \ \ \ \ \ Div[\(\(↓\)\(x\)\), \ \(\(↓\)\(y\)\), \ \(\(↑\)\(rem\)\), \ \(\(↑\)\(quo\)\)], 
		\ \ \ \ \ \ \ \ \ \ \ \ \ Pre -> \((\((x ≥ 
                0)\) ∧ \((y > 
                0)\))\), 
		\ \ \ \ \ \ \ \ \ \ \ \ \ Post -> \((\((quo*y + rem = x)\) ∧ \((0 ≤ rem < 
                y)\))\)]\)

\(Program["Division", 
	
      Div[\(\(↓\)\(x\)\), \ \(\(↓\)\(y\)\), \ \(\(↑\)\(rem\)\), \ \(\(↑\)\(quo\)\)], 
	\ \ \ \ \ \ \ \ \ quo := 0; 
	\ \ \ \ \ \ \ \ \ rem := 
        x; 
	\ \ \ \ \ \ \ \ \ WHILE[
        y ≤ rem, 
			rem := 
          rem - y; \ 
			quo := 
          quo + 1, 
			Invariant -> 
				\((\((quo*y + rem = 
                  x)\) ∧ 
				\ \ \ \ \ \ \ \ \ \ \ \ \((0 ≤ 
                  rem)\) ∧ 
				\ \ \ \ \ \ \ \ \ \ \ \ \((0 < y)\))\), 
			TerminationTerm -> 
          rem], 
		Specification -> 
        Specification["Division"]]\)

Interpretor

Example: executing the above program

Execute[Div[55,  14,  rm,  qt]]; {rm, qt}

Verification Condition Generator

Example: generating the verification conditions for  the above program

VCG[Program["Division"], Specification["Division"]]

Approach : Hoare Logic, Weakest Precondition 
(by Martin Kirchner, based on B.Buchberger)

{P}					                                      {P}
			                                                                ←(Subscript[wp, n])
(Subscript[s, 1])							                 (Subscript[s, 1])   
   ←?									       				       ←(Subscript[wp, n - 1])
(Subscript[s, 2])							                 (Subscript[s, 2])  
 ←?			  =>Weakest Precondition Strategy	       ↑ + ({{Verification}, {conditions}})                   .                                                                                                                                     
  ⋮									              			     ⋮
   ←?		                                                                                       				         ←(Subscript[wp, 1])  	
(Subscript[s, n])							                 (Subscript[s, n]) 
{Q}							                {Q}
						      
						      	               P => (Subscript[wp, n])

Generation of Loop Invariants using Combinatorics

Example: Integer  division - with WHILE loop-

quo := 
        0;
\(	\ \ \ \(rem := x;\)\)
\(	\ \ \ WHILE[
      y ≤ rem, 
	\ \ 		rem := 
        rem - y; \ 
			quo := quo + 1]\)

We obtain the following recursion equations:

(Subscript[quo, 0]) = 0                                       (Subscript[rem, 0]) = x

(Subscript[quo, k + 1]) = (Subscript[quo, k]) + 
          1                       (Subscript[rem, k + 1]) := 
        (Subscript[rem, k]) - y

Explicit equations (by using combinatorics):

(Subscript[quo, k]) = k                                         (Subscript[rem, k]) = x - k*y

Eliminate k:

rem = x - quo*y

Solution: Gosper Algorithm

How does it work?

Formula[\("Gauss", 
	∑\+\(k = 0, …, n - 1\)k\)]

Simplify[Formula["Gauss"], 
      by -> PauleSchorn–Telescope]

How can it be used for Invariant Generation (in colaboration with the Combinatorics Group from RISC)

Having:
	(Subscript[s, n + 1])=(Subscript[s, n])+ (Subscript[t, n])   =>  (Subscript[s, n + 1]) - (Subscript[s, n])= (Subscript[t, n])

(Subscript[s, n])= (Subscript[s, 0])+(Overscript[(∑_(k = 0)), n - 1])(Subscript[t, k])

⇓ GOSPER alg.

\(TraditionalForm\`\(\(	\)\(s\_n\)\)\)= (Subscript[s, 0])+GosperSum[(Subscript[t, k]),  {k, 0, n - 1}]

Invariant from Independent Recursive Equations

(Subscript[quo, 0]) = 0                                       (Subscript[rem, 0]) = x

(Subscript[quo, k + 1]) - 
        (Subscript[quo, k]) = 1                       (Subscript[rem, k + 1]) - (Subscript[rem, k]) = y

Using Gosper Alg. (Theorema`s Paule-Schorn package):

(Subscript[quo, 0]) = 0                                        (Subscript[rem, 0]) = x

(Subscript[quo, k]) = (Subscript[quo, 0]) + 
          k                            (Subscript[rem, k]) = 
        (Subscript[rem, 0]) - k*y

Eliminate k:

rem = x - quo*y

In Theorema` VCG

\(Specification["Division", 
		\ \ \ \ \ \ \ \ \ \ \ \ \ Div[\(\(↓\)\(x\)\), \ \(\(↓\)\(y\)\), \ \(\(↑\)\(rem\)\), \ \(\(↑\)\(quo\)\)], 
		\ \ \ \ \ \ \ \ \ \ \ \ \ Pre -> \((\((x ≥ 
                0)\) ∧ \((y > 
                0)\))\), 
		\ \ \ \ \ \ \ \ \ \ \ \ \ Post -> \((\((quo*y + rem = x)\) ∧ \((0 ≤ rem < 
                y)\))\)]\)

\(Program["Division", 
	
      Div[\(\(↓\)\(x\)\), \ \(\(↓\)\(y\)\), \ \(\(↑\)\(rem\)\), \ \(\(↑\)\(quo\)\)], 
	\ \ \ \ \ \ \ \ \ quo := 0; 
	\ \ \ \ \ \ \ \ \ rem := 
        x; 
	\ \ \ \ \ \ \ \ \ WHILE[
        y ≤ rem, 
			rem := 
          rem - y; \ 
			quo := 
          quo + 1, 
			TerminationTerm -> 
          rem], 
		Specification -> 
        Specification["Division"]]\)

Verification Condition Generator

VCG[Program["Division"]]

The Old Version's Verif.Conds

VCG[Program["Division"]]

Invariant from Dependent Recursive Equations

Example: Integer Square Root

The Source Code and VCs

\(Specification["Integer Square Root", 
      IntRootSpec[\(\(↓\)\(n\)\), \(\(↑\)\(k\)\)], 
	
      Pre -> \((\((n ≥ 0)\))\), 
	
      Post -> \((k ≥ 0 ∧ 
            k\^2 ≤ n\^2 ≤ \((k + 1)\)\^2)\)]\)

\(Program["Integer Square Root", 
      IntRoot[\(\(↓\)\(n\)\), \(\(↑\)\(k\)\)], 
	
      Module[{j, m}, 
		k := 0; 
		j := 1; 
		m := 1; 
		WHILE[
          m ≤ n, 
			k := k + 1; 
			j := 
            j + 2; 
			m := 
            m + j, 
			 (*\(Invariant -> \((\((k\^2 ≤ 
                      n)\) ∧ \((m = \((k + 1)\)\^2)\) ∧ \((j = 
                      2*k + 1)\) ∧ \((k ≥ 
                      0)\))\)\)\(,\)*) 
			TerminationTerm -> \((n - 
                m)\)
		]
	]
]\)

VCG[Program["Integer Square Root"], 
      Specification["Integer Square Root"]]

The Old version's VCs

VCG[Program["Integer Square Root"], 
      Specification["Integer Square Root"]]

Invariant from Mutual Recursive equations

Invariant from Mutual Recursive Equations
(ongoing work)

Having a sequence in the body of a loop:

{({{(Subscript[U, n]) = 
                    2  (Subscript[V, n - 1]) + 
                      (Subscript[U, n - 2]) (n ≥ 2),  (Subscript[U, 0]) = 1,  
                  (Subscript[U, 1]) = 0}, {(Subscript[V, n]) = 
                    (Subscript[U, n - 1]) + 
                      (Subscript[V, n - 2]) (n ≥ 2),     (Subscript[V, 0]) = 
                    0,  (Subscript[V, 1]) = 1}})

(Subscript[Solution, 2]): Generating Functions

(Subscript[U, n]) = 2  (Subscript[V, n - 1]) + (Subscript[U, n - 2]) + [n = 0],  
    (Subscript[V, n]) = (Subscript[U, n - 1]) + (Subscript[V, n - 2]) ,  n ≥ 0.

⇓

U (z) = 2 V (z) + (z^2) U (z) + 1, 
    V (z) = 
      z U (z) + (z^2) V (z)

⇓ generating functions and V(z)=((z U(z))/(1 - (z^2)))

U (z) = ((1 - (z^2))/(1 - 4 (z^2) + (z^4)));  
    V (z) = (z/(1 - 4 (z^2) + (z^4)))

Future Work

Execution: treatment of transient  arguments, exchange of parameter values between subprograms

Generation of Termination Terms

Computational Time Analysis