---
# System prepended metadata

title: TP Formel 1

---

# TP Formel 1

Maylis de Talhouet
Paco Pompeani

## Exercice 2

```
MACHINE
    machine_1
VARIABLES
    aa, bb, cc
INVARIANT 
   bb :   {2,3,4,5,6,7,8,9,10} &
   aa : {1,2,3,4,5,6,7,8,9,10} &
   cc :     {3,4,5,6,7,8,9,10} &
   max({aa,bb,cc}) : {1,2,3,4,5,6,7,8,9,10} 
   
INITIALISATION 
   aa,bb,cc := 1,2,3
END
```

Atelier B n'a pas pu prouver l'appartenance de `bb` à l'ensemble d es entiers naturels. Cette appartenance est triviale donc on valide cette PO.

### POs WellDefinednessInvariant

```
--------------------
        bb: {2,3,4,5,6,7,8,9,10} &
        aa: {1,2,3,4,5,6,7,8,9,10} &
        cc: {3,4,5,6,7,8,9,10} &
        "Well definedness" 
=>
        not({aa,bb,cc} = {}) 
--------------------
        bb: {2,3,4,5,6,7,8,9,10} &
        aa: {1,2,3,4,5,6,7,8,9,10} &
        cc: {3,4,5,6,7,8,9,10} &
        "Well definedness" 
=>
        {aa,bb,cc}/\NATURAL: FIN(NATURAL) 
```
## Exercice 3

```
MACHINE
    exercice_3 /* service de reservation de places */
VARIABLES
    nbPlaceLibre
INVARIANT
    nbPlaceLibre : NAT &
    nbPlaceLibre >= 0 &
    nbPlaceLibre <= 10
INITIALISATION
    nbPlaceLibre := 10
OPERATIONS
    reserver =
    PRE
        nbPlaceLibre > 0
    THEN
        nbPlaceLibre := nbPlaceLibre - 1
    END
END
```

Les 6 POs (3 d'initialisation et les 3 de reserver) ont pu être prouvées par l'Atelier B sans travail supplémentaire.

### POs WellDefinednessInvariant


```
--------------------
        "Invariant is preserved" &
        "Check invariant ((nbPlaceLibre) : (NAT))" 
=>
        nbPlaceLibre-1: NAT 
--------------------
        "Invariant is preserved" &
        "Check invariant (0 <= nbPlaceLibre)" 
=>
        0<=nbPlaceLibre-1 
--------------------
        "Invariant is preserved" &
        "Check invariant (nbPlaceLibre <= 10)" 
=>
        nbPlaceLibre-1<=10 
```