## Conjugate of a partition

Authors: Jean-Christophe Filliâtre

Topics: Ghost code

Tools: Why3

see also the index (by topic, by tool, by reference, by year)

```(*
Conjugate of a partition.

Author: Jean-Christophe Filliatre (CNRS)

A partition of an integer n is a way of writing n as a sum of positive
integers. For instance 7 = 3 + 2 + 2 + 1. Such a partition can be
displayed as a Ferrer diagram:

3 * * *
2 * *
2 * *
1 *

The conjugate of that a partition is another partition of 7, obtained
by flipping the diagram above along its main diagonal. We get

4 * * * *
3 * * *
1 *

Equivalently, this is the number of cells in each column of the original
Ferrer diagram:

4 3 1
3 * * *
2 * *
2 * *
1 *

The following program computes the conjugate of a partition.
A partition is represented as an array of integers, sorted in
non-increasing order, with a least a 0 at the end.

Franck Butelle, Florent Hivert, Micaela Mayero, and Frédéric
Toumazet. Formal Proof of SCHUR Conjugate Function. In Proceedings
of Calculemus 2010, pages 158-171. Springer-Verlag LNAI, 2010.
*)

module Conjugate

use int.Int
use ref.Refint
use array.Array

predicate is_partition (a: array int) =
(* at least one element *)
a.length > 0 &&
(* sorted in non-increasing order *)
(forall i j: int. 0 <= i <= j < a.length -> a[i] >= a[j]) &&
(* at least one 0 sentinel *)
a[a.length - 1] = 0

(* values in a[0..n[ are > v, and a[n] <= v *)
predicate numofgt (a: array int) (n: int) (v: int) =
0 <= n < a.length &&
(forall j: int. 0 <= j < n -> v < a[j]) &&
v >= a[n]

predicate is_conjugate (a b: array int) =
b.length > a[0] &&
forall j: int. 0 <= j < b.length -> numofgt a b[j] j

let conjugate (a: array int) : array int
requires { is_partition a }
ensures  { is_conjugate a result }
=
let b = Array.make (a[0] + 1) 0 in
let partc = ref 0 in
while a[!partc] <> 0 do
invariant { 0 <= !partc < a.length }
invariant { forall j: int. a[!partc] <= j < b.length -> numofgt a b[j] j }
variant   { a.length - !partc }
label L in
let ghost start = !partc in
let edge = a[!partc] in
incr partc;
while a[!partc] = edge do
invariant { start <= !partc < a.length }
invariant { forall j: int. start <= j < !partc -> a[j] = edge }
variant   { a.length - !partc }
incr partc
done;
for i = a[!partc] to edge - 1 do
invariant { forall j: int. edge <= j < b.length -> b[j] = (b at L)[j] }
invariant { forall j: int. a[!partc] <= j < i -> b[j] = !partc }
b[i] <- !partc
done
done;
assert { a[!partc] = 0 };
b

end

module Test

use int.Int
use array.Array
use Conjugate

let test () ensures { result.length >= 4 } =
let a = make 5 0 in
a[0] <- 3; a[1] <- 2; a[2] <- 2; a[3] <- 1;
conjugate a

exception BenchFailure

let bench () raises { BenchFailure -> true } =
let a = test () in
if a[0] <> 4 then raise BenchFailure;
if a[1] <> 3 then raise BenchFailure;
if a[2] <> 1 then raise BenchFailure;
if a[3] <> 0 then raise BenchFailure;
a

end

(*
Original C code from SCHUR

Note that arrays are one-based
(that code was translated from Pascal code where arrays were one-based)

#define MAX 100

void conjgte (int A[MAX], int B[MAX]) {
int i, partc = 1, edge = 0;
while (A[partc] != 0) {
edge = A[partc];
do
partc = partc + 1;
while (A[partc] == edge);
for (i = A[partc] + 1; i <= edge; i++)
B[i] = partc - 1;
}
}
*)
```