Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

Commit b375b98c authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

new example: conjugate of a partition

parent 666aeb68
(*
Conjugate of a partition.
Author: Jean-Christophe Filliatre (CNRS)
A partition of an integer n is a wy 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.
This was inspired by this article:
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 import ref.Refint
use import 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 }
'L:
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] = (at b 'L)[j] }
invariant { forall j: int. a[!partc] <= j < i -> b[j] = !partc }
b[i] <- !partc
done
done;
assert { a[!partc] = 0 };
b
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;
}
}
*)
\ No newline at end of file
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment