Two equal elements

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

Short Description

Given: An integer array a of length n+2 with n>=2. It is known that at
least two values stored in the array appear twice (i.e., there are at
least two duplets).

Implement and verify a program finding such two values.

You may assume that the array contains values between 0 and n-1.

Example:

Array: [0, 1, 2, 3, 4, 5, 4, 5]

Output: 4, 5

Code

Specification

Long Description

This challenge is a popular “job interview-style” question, but we
are not aware of its origin. The challenge was selected as it requires complicated array reasoning, specifications, and invariants.

Supplementary Materials

This problem was posed as challenge 3 at the COST Verification Competition 2011. The time given for solving this challenge during the competition was 90 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

Author

Wojciech Mostowski and Christoph Scheben

Code/Specification

The key point in the solution of this challenge is to be able to specify the number of occurrences of an element in the array (and reason about it). In JML, this can be done with the help of the \sum operator, a special quantifier that provides an arithmetic sum over the quantified elements. First, the team defined a method to count the number of occurrences of a given element in the array with the following simple specification:

//@ ensures \result ==
//@
(\sum int i; 0<=i && i<a.length; a[i] == value ? 1 : 0);
static int /*@ pure @*/ countAcc(int[] a, int value) {...}

The implementation of the method uses a simple loop annotated with appropriate JML specifications to count the elements.

Solution-problem relationship

The team used the method method to count the number of occurrences of a given element in the array to implement and specify the top-level method that finds the two values that are each duplicated in the array. The solution was developed for a slightly more general case, where it was not assumed that the elements in the array are all between 0 and n − 1. Instead, only the existence of two pairs of duplicates from an arbitrary range of integers smin..smax
(smin+1<smax) is required by the precondition of the top-level method.
The postcondition of the top-level method states that the two duplicated
elements are found. The implementation of the method iterates over all values in
the smin..smax range, calls countAcc to get the count of the current value, and
terminates once a second duplicated value has been found. The most difficult part
is expressing the invariant for the iteration loop. It makes a case distinction over how many duplicate elements has been found so far and specifies a corresponding condition about the elements yet-to-be found.

Interactivity, effort needed

KeY proves the method to count the number of occurrences of a given element in the array correct automatically within a few seconds.
The proof for the top-level method requires some minor interactions (more or less obvious quantifier instantiations), while the rest is done automatically within 10 seconds.

How to reproduce

You can access the latest version of KeY via Webstart.

Published

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

Submitted by

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