Sum and Maximum

July 1, 2012 – 4 years, 9 months ago, by vladimir

Short Description

Given an N-element array of natural numbers, write a program to compute the sum and the maximum of the elements in the array.

Code

int sum, max = 0;
int i;
for (i=0; i<N; i++){
  if (max < a[i]){
    max = a[i];
  }
  sum += a[i];
}

Specification

Given that N>=0 and a[i]>=0 for 0<= i< N, prove the post-condition that sum<=N*max.

Long Description

Supplementary Materials

Test Case: With the array 9, 5, 0, 2, 7, 3, 2, 1, 10, 6, N is 10, max is 10, and the sum is 45.

This problem was posed at the VSTTE'10 verification competition by Peter Müller <Peter.Mueller@inf.ethz.ch> and Natarajan Shankar <shankar@csl.sri.com>.

If you want to attach a file, please attach to this page and post a link here.

Submitted by

Vladimir Klebanov <verifythis@cost-ic0701.org>


Solution

Tool/Method

KeY. (Webstart)

An automated/interactive tool for Java source code verification using dynamic logic.

Code/Specification

The formalisation is a straight-forward JML specification for the canonical Java version of the pseudo code.

Since multiple return values are not supported by Java, we store the result in instance variables max and sum.

Annotated MaxSum.java available in the solutions ZIP.

Solution-problem relationship

In addition to the required post-condition sum <= a.length * max, we have added the properties that one would usually expect of the sum and the maximum.

Interactivity, effort needed

The problem was solved by the KeY team during the VSTTE'10 competition.

Technically, KeY is able to find the proof automatically (given the annotations) in some 6 seconds.

How to reproduce

You can load the evidence file (MaxSum.java.proof) into the web start version of KeY linked above. This will provide you with a complete proof script in dynamic logic. Though KeY supports calls to SMT solvers like Z3, this was not needed in this case.

Published

http://www.vscomp.org

Submitted by

Vladimir Klebanov <verifythis@cost-ic0701.org>


Solution

Tool/Method

Holfoot

Code/Specification

The program is written in Holfoot's imperative programming language, which is a tiny subset of C. The specification requires procedure specifications as well as a specification of the loop. There are three specifications available:

Solution-problem relationship

Holfoot supports just a tiny subset of C. This subset is, however, formalised in the HOL 4 theorem prover and after parsing, all verification steps are done by proof inside HOL 4. Some syntax used in the pseudo code is not available. Thus, the for-loop has been replaced by a while-loop. Furthermore, the syntax "a[i]" is not available for arrays. Instead "(a + i)->dta" is used. Finally, a variable tmp is introduced to hold the value of "a[i]", because Holfoot requires heap lookups to be separate instructions. Otherwise the implementation is straightforward.

There are 3 different specifications available. The simple one just establishes the required post-condition "sum <= length * max". Moreover, it is guaranteed, that the array is unchanged and that no memory leak / null pointer exception etc. occurred. Termination is, however, not proofed. Unluckily, the HOL 4 theorem prover is bad with arithmetic. Therefore, the proof requires 7 lines of a simple, interactive proof script to handle the occuring arithmetic. The structure of the program is handled automatically, though.

In order to demonstrate the benefits of using an interactive theorem prover, functions for the maximum and length of a list are then defined. Given these definition a general theorem

forall l. LIST_SUM l <= (LENGTH l) * LIST_MAX l
can be proved independently of the code. Given this theorem, the "interactive" proof consists of calling the automation followed by a call to the HOL 4 simplifier with the definition of these new functions.

For comparison there is a specification using an loop-invariant and one using a loop-specification. In this example, it does not matter much, which type of loop annotation is used. The loop-invariant states that the sum / maximum up the the current index has been calculated. The loop-specification states that everything after the current index still needs processing. Both statements are easy to express. In this case, the invariant might be simpler. However, proving it requires two tiny lemmata about adding an element at the end of a list when computing the sum and maximum.

Interactivity, effort needed

The problem was solved during the VSTTE'10 competition. Unluckily, it took much longer than it should. HOL 4 is bad at arithmetic and I'm not very familiar with the arithmetic libraries. Therefore, proving this trivial theorem about "sum < length * max" took me about 45 minutes. Having found the appropriate theorems in the list libraries I would guess writing the program and doing the proof should be doable in 20 minutes.

How to reproduce

The example is available with Holfoot. It is easiest to use the Webinterface to run the example. However, one can download the sources and run the example inside HOL 4 as well.

Published

Submitted by

Thomas Tuerk


Solution

Author

K. Rustan M. Leino

Tool/Method

Dafny

Code/Specification

Dafny is an object-based language with built-in specification constructs.
To a first approximation, it is like Java (but without subclasses) with Eiffel- or JML-like specifications. Language features that are especially useful when writing specifications include sets and sequences, ghost variables, and user-defined recursive functions.
Dafny uses mathematical integers (implemented by big-nums), which avoids overflow errors.

Solution-problem relationship

The solution is a straightforward translation of the problem into the specification language.

Interactivity, effort needed

The problem was solved during the VSTTE'10 competition.

How to reproduce

The solution can be found on the webpage. It includes a file "VSComp-Leino-1.dfy" which can be run with the Dafny tool.

Published

http://www.vscomp.org/

Submitted by

Sarah Grebing (based on the competition experience report published on the webpage)


Solution

Author

Rosemary Monahan and Nadia Polikarpova

Tool/Method

Boogie2

Code/Specification

Boogie2 is an intermediate verification language designed to accommodate the encoding of verification conditions for imperative, object-oriented programs.

Solution-problem relationship

We did not prove termination for any of the problems as Boogie2 does not directly support termination measures.

Interactivity, effort needed

The problem was solved during the VSTTE'10 competition.

Our solution to this problem was easily specified and automatically verified in less than 2 seconds. Our main observation here was that specifications for small, integer- and array-manipulating programs in Boogie2 are simple and concise.

How to reproduce

The solution can be found on the webpage. It includes the file "problem1.bpl" which can be run with the Boogie2 tool.

Published

http://www.vscomp.org/

Submitted by

Sarah Grebing (based on the competition experience report published on the webpage)