Questa è una vecchia versione del documento!
Indice
S3 - Progetto finale
Testo e norme
Si trovano qui
FAQ
E' opportuno prevedere più sistemi SPARK?
Sì, almeno perché la parte di aggiornamento del codice di controllo non può aggiornare se stessa, per via della natura fortemente statica del linguaggio.
Come si crea una matrice di variabili di confine?
Dato che i package non sono oggetti di prim'ordine in SPARK, bisogna simulare la matrice con una funzione che mappa gli indici su uno specifico package. Per esempio, per le temperature, il secondo sensore del quarto appartamento sarà rappresentato da
package Temp_4_2; –# own in T; end package Temp_4_2;
e il package Edificio avrà una funzione getTemp(noSensore : … ; noAppartamento : … ) return Temperatura;
che conterrà un mostruoso case (peraltro generabile automaticamente), tra cui
… if noAppartamento = 4 and noSensore = 2 then ret := Temp_4_2.T else …
Dal punto di vista INFORMED, la situazione si presenta così:
