la méthode SumMax

Compléter pour obtenir une solution validée par Dafny.

method SumMax(x: int, y: int) returns (s: int, m: int)
    ensures s==x+y
    ensures x <= m && y <= m
    ensures m==x || m==y
{
    ...
}

à propos du maximum de deux entiers relatifs

On considère les deux relations suivantes, dont les arguments sont des entiers relatifs.

F(x,y,m) : m == (if x < y then y else x)
G(x,y,m) : x <= m && y <= m && (m == x || m ==y)

Montrer qu'elles sont équivalentes.

les méthodes SumMaxBackwards

Compléter et proposer deux solutions distinctes validées par Dafny.

method SumMaxBackwards(s:int, m :int) returns (x:int, y:int)
    requires ...
    ensures s==x+y
    ensures x <= m && y <= m
    ensures m==x || m==y
{
    ...
}

la méthode CountToAndReturnN

Compléter pour obtenir une solution validée par Dafny.

method CountToAndReturnN(n: int) returns (r: int)
    requires ...
    ensures r == n 
{
    var i := 0;
    while i < n
      ...
    {
        i := i + 1;
    }
    r := i;
}

les méthodes Min2 et Min3

Compléter pour obtenir une solution validée par Dafny. Proposer plusieurs solutions pour Min3.

method Min2(x: int, y: int) returns (m:int)
    requires ...
    ensures ... // m est le min de x et y
{
    ...
}

method Min3(x: int, y: int, z: int) returns (m:int)
    requires ...
    ensures ... // m est le min de x, y et z
{
    ...
}

la fonction Fib et la méthode ComputeFib

Compléter pour obtenir une solution validée par Dafny.

function Fib(n: nat): nat
{
    if n < 2 then n else Fib(n-1) + Fib(n-2)
}

method ComputeFib(n: nat) returns (x:nat)
    ensure x == Fib(n)
{
    ...
}

la fonction Sum et la méthode ComputeSum

Considérer le code ci-dessous.
Montrer par récurrence sur n que Sum(n) est la somme des entiers de 0 à n inclus.
Compléter pour obtenir une solution validée par Dafny.

function Sum(n: nat): nat
{
    if n == 0  then 0 else n + Sum(n-1)
}

method ComputeSum(n: nat) returns (s:nat)
    ensures s == Sum(n)
{
    ...
}

la fonction Fact et la méthode ComputeFact

Compléter pour obtenir une solution validée par Dafny.

function factorial (n: nat): nat 
{
    if n == 0 then 1 else n*factorial(n - 1)
}

method computeFactorial(n: nat) returns (f: nat)
    ensures f == factorial(n)
{
    ... 
}

une méthode Carre pour élever un entier au carré

Considérer le code ci-dessous. Montrer que

0 ≤ i ≤ a est un invariant de boucle
c == i*i est un invariant de boucle
la quantité a-i est un variant de boucle

Compléter pour obtenir une solution validée par Dafny.
Généraliser pour un argument entier relatif.

method Carre(a: nat) returns (c: nat)
ensures c == a*a
{
  var i := 0;
  c := 0;
  while i != a
    ...
  {
    c := c + 2*i +1;
    i := i + 1;
  }
}

Une méthode Mult pour multiplier deux entiers

Considérer le code ci-dessous. Montrer que

x ≥ 0 est un invariant de boucle
y ≥ 0 est un invariant de boucle
x + y*b == a*b est un invariant de boucle
la quantité y est un variant de boucle

Compléter pour obtenir une solution validée par Dafny.
Généraliser pour deux arguments entiers relatifs.

method Mult(a: nat, b:nat) returns (m:nat)
    ensures m == a*b
{
  var x, y := 0, a;
  while y!= 0 
  ...  
  {
    x := x+b;
    y := y-1;
  }
  m := x;
}

Une méthode Somme pour ajouter deux entiers naturels

Considérer le code ci-dessous.
Déterminer un invariant de boucle, par exemple en décomposant la post-condition.
Déterminer un variant de boucle.
Compléter le code pour obtenir une solution validée par Dafny.

method Sum(a: nat, b: nat) returns (s: nat)
ensures s == a+b
{
  var x, y := a, b;
  while y != 0
        ...
  {
    x := x+1;
    y := y-1;
  }
  s := x;
}

une méthode de recherche linéaire pour les tableaux d'entiers

Compléter pour obtenir une solution validée par Dafny.

method LinearSearch(a:array<int>, key:int) returns (r:int)
  requires ...
  ensures 0 <= r ==> r < a.Length && a[r]==key
  ensures r < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != key
{
    ...
}

une méthode MaxArray pour les tableaux d'entiers

Ecrire et valider en Dafny une methode Max qui prend en entrée un tableau d'entiers non-vide et renvoie son plus grand élément. Formaliser la post-condition avec des ensures.

method MaxArray(a: array<int>) returns (max: int)
    requires 1 <= a.Length
    ensures ...
{
    ...
}

une fonction Sum_array pour les tableaux d'entiers

Ecrire en Dafny une fonction logique Sum_array(i,a) qui somme les éléments d'indice 0 à i inclus du tableau non-vide a.
Par récurrence finie sur i, montrer que cette fonction est correcte.
Quelle est la valeur de Sum_array(a.Length-1,a) ?

function Sum_array(i:int, a:array<int>): int
    requires 0 <= i < a.Length 
    ...

une méthode SumArray pour les tableaux d'entiers

Ecrire et valider en Dafny une methode SumArray qui prend en entrée un tableau d'entiers non-vide et renvoie la somme de ses éléments.

method SumArray(a: array<int>) returns (sum: int)
    requires 1 <= a.Length
    ensures sum == Sum_array(a.Length-1,a)
    ...

une méthode MinMaxSum pour les tableaux d'entiers

Ecrire et valider en Dafny une methode MinMaxSum qui prend en entrée un tableau d'entiers non-vide et renvoie son plus petit élément, son plus grand élément et la somme de ses éléments tout en garantissant les post-coditions ci-dessous :

method MinMaxSum(a:array<int>) returns (min:int, max:int, sum:int)
    requires 1 <= a.Length
    ensures a.Length * min <= sum <= a.Length * max
    ensures forall i :: 0 <= i < a.Length ==> a[i] <= max
    ensures exists i :: 0 <= i < a.Length  && a[i] == max
    ensures forall i :: 0 <= i < a.Length ==> a[i] >= min
    ensures exists i :: 0 <= i < a.Length  && a[i] == min
    ensures sum == Sum_array(a.Length-1,a)
    ...

une méthode de recherche dichotomique dans un tableau d'entiers trié

Considérer le code ci-dessous.
Exprimer la précondition et les post-conditions en langage naturel.
Exprimer les invariants et le variant de la boucle en langage naturel.
Compléter pour obtenir une solution validée par Dafny.

method BinarySearch(a:array<int>, key:int) returns (r:int)
    requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j]
    ensures 0 <= r ==> r < a.Length && a[r]==key
    ensures r < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != key
{
    var lo, hi := 0, a.Length;
    while lo < hi 
        invariant 0 <= lo <= hi <= a.Length
        invariant forall i :: 0 <= i < lo ==> a[i] != key
        invariant forall i :: hi <= i < a.Length ==> a[i] != key
        decreases hi - lo
    {
    ...
    }
}

une méthode alternative de recherche dichotomique dans un tableau d'entiers trié

Cette méthode ne renvoie plus de valeurs négatives mais l'indice où la clé devrait être insérée dans le tableau pour qu'il reste trié. Donc les éléments a[i] du tableau situés à gauche de r sont tels que a[i] < key et les éléments a[j] du tableau situés à droite de r sont tels que a[j] >= key.
Exprimer la précondition et les post-conditions en langage naturel.
Exprimer les invariants et le variant de la boucle en langage naturel.
Compléter pour obtenir une solution validée par Dafny.

method BinarySearch_bis(a:array<int>, key:int) returns (r:int) 
    requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j]
    ensures 0 <= r <= a.Length
    ensures r < a.Length ==> forall i,j :: 0 <= i < r <= j < a.Length ==> a[i] < key <= a[j]
    ensures r == a.Length ==> forall i :: 0 <= i < r ==> a[i] < key
{
    var lo, hi := 0, a.Length;
    while lo < hi 
        invariant 0 <= lo <= hi <= a.Length
        invariant forall i :: 0 <= i < lo ==> a[i] < key
        invariant forall i :: hi <= i < a.Length ==> key <= a[i] 
        decreases hi - lo
    {
        ...
    }
    return lo;
}

la méthode DutchFlag

Considérer le code ci-dessous. Le prédicat Below est-il

correct : si il est vrai, l'ordre des couleurs en argument est valide ?
complet : si l'ordre des couleurs en argument est valide, le prédicat est vrai ?

Compléter pour obtenir une solution validée par Dafny.

datatype Color = Red | White | Blue
    
predicate Below(c: Color, d: Color)
    {
      c == Red || c == d || d == Blue
    }

method DutchFlag(a: array<Color>)
      modifies a
      ensures forall i,j :: 0 <= i < j < a.Length  ==>  Below(a[i], a[j])
      ensures multiset(a[..]) == multiset(old(a[..]))
    {
      var r, w, b := 0, 0, a.Length;
      while w < b
        invariant 0 <= r <= w <= b <= a.Length;
        invariant forall i :: 0 <= i < r ==> a[i] == Red
        invariant forall i :: r <= i < w ==> a[i] == White
        invariant forall i :: b <= i < a.Length ==> a[i] == Blue
        invariant multiset(a[..]) == multiset(old(a[..]))
      {   match a[w]
            case Red =>
            ...
            case White =>
            ...
            case Blue =>   
            ...
      }
    }

On pourra tester ce code comme suit :

method Main()
    {
      var a := new Color[3];
      a[0] := White;
      a[1] := Blue;
      a[2] := Red;
      assert a[..] == [White, Blue, Red];
      DutchFlag(a);
      assert Below(a[0], a[1]);
      assert Below(a[1], a[2]);
      assert a[..] == [Red, White, Blue];
    }

une méthode de tri d'un tableau de booléens

Considérer le contrat ci-dessous. Expliciter les deux post-conditions. Compléter le code pour obtenir une solution validée par Dafny.

method tri_tab_bool(a: array<bool>)
    modifies a
    ensures forall m,n :: 0 <= m < n < a.Length ==> (!a[m] || a[n])
    ensures multiset(a[..]) == multiset(old(a[..]))
{
    var lo, hi := 0, a.Length - 1;
    while (lo < hi)
    ...
}