## Selection sort

*June 22, 2010 – 6 years, 10 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