/* une diée de ce qui était attendu ...
1- Preuves :

2- Prolog :

listeBONUS(LISTEBONUS) :-

             listeEtudiants(L), % pour passer de l'ensemble des faits étudiant/3 à la liste L des termes étudiant/3 cf. exemple de l'énoncé

             listeEtudiantsRendusSup2MAX(L ,L1),  % pour passer de la liste des termes étudiant/3  L à la liste L1 des termes étudiant/5

             listeB(L1 , LISTEBONUS).  % on balaye la liste L1 des termes étudiant/5  pour construire la liste des termes bonus/3 demandée

listeB([] , []).

listeB([étudiant(N , M , _ , _ , Sup2 , MAX) | L] , [bonus(N , M , 3) | LB] ) :- compare(> , Sup2, 8) , compare(> , MAX, 3) ,!, listeB(L ,LB) .

listeB([étudiant(N , M , _ , _ , SUP2 , _) | L] , [bonus(N , M , 2) | LB] ) :- compare(> , SUP2 , 7) , !, listeB(L ,LB) .

listeB([étudiant(N , M , _ , Rendus , _ , _) | L] , [bonus(N , M , 1) | LB] ) :- compare(> , Rendus , 9) , !, listeB(L ,LB) .

listeB([étudiant(N , M , _ , _ , _ , _) | L] , [bonus(N , M , 0) | LB] ) :- listeB(L ,LB) .

3-Logique de HOARE :

Q1 : de Java+ESC/JAVA à HOARE

{ n >= 1}

m := MAX_VALUE;

{ 'A' k; k>=0 & k<n -> a[k]<m)}

mindex := 0; i:=0;

{ 'A' k; k>=0 & k<n -> a[k]<m) & i=0 & mindex = 0}

while(i<n)

      invariant ('A' k : k>=0 & k<i -> m<=a[k]) & 0 <= mindex & mindex <= i & i>=0 & i<=n

     variant n-i;

do if (a[i] < m) then mindex = i;m = a[i] end ; i := i+1 end

{'A' k; k>=0 & k<n -> m<=a[k] & 0 <= mindex & mindex <= n);

Q2 : 5 obligations de preuves selon les 5 points du canevas

(i)( 'A' k :  k>=0 & k<n -> a[k]<m) & i=0 & mindex = 0) -> (('A' k : k>=0 & k<i -> m<=a[k]) & 0 <= mindex & mindex <= i & i>=0 & i<=n)

(ii)invariant de la boucle(en remontant)

(('A' k : k>=0 & k<i -> m<=a[k]) & 0 <= mindex & mindex <= i & i>=0 & i<=n & i<n)

while(i<n) do if (a[i] < m) then mindex = i;m = a[i] end ; i := i+1 end

('A' k : k>=0 & k<i -> m<=a[k]) & 0 <= mindex & mindex <= i & i>=0 & i<=n

(iii)post condition

(('A' k : k>=0 & k< i -> m<=a[k]) & 0 <= mindex & mindex <= i & i>=0 & i<=n & i>=n )

-> (('A' k :  k>=0 & k<n -> m<=a[k] )& 0 <= mindex & mindex <= n))

(iv)ARRET de la boucle :

(('A' k : k>=0 & k<i -> m<=a[k]) & 0 <= mindex & mindex <= i & i>=0 & i<=n & i<n)  -> (n-i>0)

(v) V:= n-i; if (a[i] < m) then mindex = i;m = a[i] end; i := i+1 {n-i<V}

Q3 : preuve du point (v)

V:= n-i;

if (a[i] < m) then mindex = i;m = a[i] end;

i := i+1

{n-i<V}  // en remontant

remarque : if (a[i] < m) then mindex = i;m = a[i] end; ne modifie pas les valeurs de i  et n donc on peut ne pas tenir compte de cette instruction dans la preuve, d'où

{n-i-1<n-i} toujours vraie...

V:= n-i;

{n-i-1<V}

i := i+1

{n-i<V}  // en remontant

class CommandeAllumerSpot implements Command {
        private Spot monSpot;
        public CommandeAllumerSpot ( Spot L) {monSpot  =  L;}
        public void execute( ) {monSpot . turnOn( );}
}
class CommandeEteindreSpot implements Command {
        private Spot monSpot;
        public CommandeEteindreSpot ( Spot L) {monSpot  =  L;}
        public void execute( ) {monSpot . turnOff( );}}
class CommandeMarcheVentilo implements Command {cf  CommandeAllumerSpot }
class CommandeStopVentilo implements Command {cf  CommandeEteindreSpot }
public class TestCommand {
                public static void main(String[] args) {
                        Spot  testSpot = new Spot( );
                        CommandeAllumerSpot testLOC = new CommandeAllumerSpot(testSpot);
                        CommandeEteindreSpot testLFC = new CommandeEteindreSpot(testSpot);
                        Interrupteur testInter = new testInter ( testLOC,testLFC);       
                        testInter.flipUp( ); testInter.flipDown( );
                        Ventilo testVentilo = new Ventilo( );
                        CommandeMarcheVentilo foc = new CommandeMarcheVentilo(testVentilo);
                        CommandeStopVentilo ffc = new CommandeStopVentilo(testVentilo);
                        Interrupteur ts = new Interrupteur( foc,ffc);ts.flipUp( ); ts.flipDown( ); 
                }}