Selection sort

June 22, 2010 – 6 years, 9 months ago, by mulbrich

Short Description

Full functional specification and verification of an implementation of selection sort.

Code

public class Sort {
    public int[] a;

    void demo() {
      int l   = a.length;
      int pos = 0;

      while (pos<l) {
          int counter = pos;
          int idx = pos;

          while (counter<l) {
              if (a[counter] > a[idx])
                  idx=counter;
              counter=counter+1;
          }
          int tmp=a[idx];
          a[idx]=a[pos];
          a[pos]=tmp;
          pos=pos+1;
      }
    }
}

Specification

After the execution of demo() the array a is

  • sorted in descending order
  • a permutation of the the array prior to the method call

Long Description

The example contains a simple implementation of the selection sort algorithm. It
will be shown that on certain preconditions the implementation works correct, i.e
the result is a sorted array that is a permutation of the given array. Consequently
the problem of verifying the implementation can be divided into the following
two subproblems:
A) How to verify that the resulting array is sorted?
B) How to verify that the resulting array is a permutation of the given array?

Supplementary Materials

Submitted by

M. Ulbrich


Solution

Tool/Method

KeY 1.4 (a special side branch version is needed to deal with permutations)

Code/Specification

The specification is expressed using JavaCard Dynamic Logic (the input logic of KeY).
The permutation property cannot be expressed in JML.

Solution-problem relationship

Full functional verification

Interactivity, effort needed

That the array is sorted in the end can be proved automatically.
One instantiation is needed to complete the proof for the permutation.

How to reproduce

see

Published

Submitted by

M. Ulbrich