Maximum in an array (by elimination)

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

Short Description

Given: A non-empty integer array a.

Verify that the index returned by the method max() given below points to
an element maximal in the array.

Code

public class Max {

    public static int max(int[] a) {
        int x = 0;
        int y = a.length-1;

        while (x != y) {
            if (a[x] <= a[y]) x++;
                else y--;
        }
        return x;
    }
}

Long Description

Motivation: This challenge is an instance of Kaldewaij’s Search by Elimination [1], where an element with a given property is located by eliminating elements that do not have that property. The challenge was selected as it involves a relatively simple but interesting invariant, expressing that the maximal element is in the remaining search space rather than maintaining the maximal element found so far.

[1] A. Kaldewaij. Programming: the derivation of algorithms. Prentice-Hall, Inc., 1990.

Supplementary Materials

This problem was posed as challenge 1 at the COST Verification Competition 2011. The time given for solving this challenge during the competition was 60 minutes.

Submitted by

Sarah Grebing (based on the challenges given in the COST Verification Competition 2011) and the report about this challenge )


Solution

Tool/Method

KeY. A highly automated, explicit-proof-object
theorem prover for Java programs based on Dynamic Logic. A version of KeY based on static frames was used in solving this challenge. The current stable release of KeY can be accessed via web start here.

Author

Wojciech Mostowski and Christoph Scheben

Code/Specification

Straight-forward JML specification.

Solution-problem relationship

The loop invariant provided by the KeY team:

(\forall int i; i>=0 && i<=x; a[i]<=a[x] || a[i]<=a[y]) &&
(\forall int j; j>y && j<a.length; a[j]<=a[x] || a[j]<=a[y]);

Interactivity, effort needed

The KeY system proves this program fully correct (including integer overflow checks) in around 10 seconds.

How to reproduce

You can load the evidence file

"JML normal_behavior operation contract (id 0 - challange1.Max__max).proof" 
into the web start version of KeY linked above. This will provide you with a complete proof script in dynamic logic.

Published

http://foveoos2011.cost-ic0701.org/verification-competition

Submitted by

Sarah Grebing (based on the Experience report about the competition)


Solution

Tool/Method

Dafny

Author

Julian Tschannen and Nadia Polikarpova

Code/Specification

Dafny is a programming language with built-in specification
constructs. A Dafny program consists of classes, which contain variables and
methods. Methods can be equipped with annotations in the form of pre- and
postconditions, inline assertions, loop invariants and termination measures for loops and recursion. Specifications may contain user-defined recursive functions, as well as ghost variables and ghost code.

Solution-problem relationship

The invariant provided by the Dafny team:

invariant ∀ i • 0 ≤ i < a . Length ∧ a [ i ] > a [ x ] ∧ a [ i ] > a [ y ] =⇒ x < i < y ;

Interactivity, effort needed

How to reproduce

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

Published

http://foveoos2011.cost-ic0701.org/verification-competition

Submitted by

Sarah Grebing (based on the Experience report about the competition)


Solution

Tool/Method

KIV

Author

Gidon Ernst, Bogdan Tofan and Gerhard Schellhorn

Code/Specification

After the competition, the team also solved this challenge using KIV’s Java
calculus.

Solution-problem relationship

The loop invariant provided by the KIV team:

∃k. x ≤ k ∧ k < y ∧ k < #ar ∧ ar [k] = max (ar )

Interactivity, effort needed

How to reproduce

More information about the abstract proof can be found here

Published

The solution in KIVs Java calculus can be found here.

Submitted by

Sarah Grebing (based on the Experience report about the competition)


Solution

Tool/Method

Why3/Krakatoa

Author

Claude Marché

Code/Specification

The code/specification can be found here

Solution-problem relationship

The loop invariant provided:

\forall integer i;
0 <= i < x || y < i < a.length ==> a[i] <= max(a[x],a[y]);

Interactivity, effort needed

How to reproduce

The solution can be found on the webpage. It includes a file "challenge1.java" which can be run with the why3/krakatoa tool.

Published

http://proval.lri.fr/gallery/ArrayMax.en.html and http://foveoos2011.cost-ic0701.org/verification-competition

Submitted by

Sarah Grebing (based on the challenges given in the COST Verification Competition 2011) and the report about this challenge )