## 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

### 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

### 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

### 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 )