Metodi formali nello sviluppo software
a.a.2013/2014
Prof. Anna Labella
12/19/2015
1
Proprietà
 |-   M |= 
Completezza M |=    |- 
Indecidibilità
Compattezza
Espressività
Correttezza
12/19/2015
2
Compattezza
 è coerente sse ogni suo s.i.
finito è coerente
Teorema
|=, allora |-,
ma questo significa che esiste un s.i.
finito  t.c.
allora |-, cioè |=
Se
12/19/2015
3
Löwenheim-Skolem
per  c’è un modello per ogni
cardinalità finita, allora ce n’è uno con
cardinalità infinita
Descriviamo le cardinalità finite: se sono
tutte coerenti con , allora c’un modello
che le soddisfa tutte e, dunque è infinito
Se
12/19/2015
4
Espressività
Good news
SQL queries su basi di dati relazionali
Xqueris su cocumenti XML
12/19/2015
5
Espressività
12/19/2015
6
Espressività
Bad news:
La raggiungibilità nei grafi diretti è decidibile?
Teorema. No: è esprimibile attraverso una formula φ?
Per il teorema di compattezza, date
definiamo
Soddisfacibile o insoddisfacibile?
Abbiamo bisogno di un linguaggio esistenziale del secondo
7
12/19/2015
ordine
Micromodelli del software

Model checking M |= 

Conseguenza logica  |= 
12/19/2015
8
Conseguenza logica  |= 
 è un insieme di richieste per il nostro
software
  una proprietà

 |=  : ogni modello di  soddisfa 
bello, ma indecidibile

12/19/2015
9
Model checking M |= 
Si
costruisce un modello M secondo le
richieste e si verifica 
Decidibile, ma si rischia di
superspecificare senza saperlo
12/19/2015
10
State machines 1

un tool: Alloy
12/19/2015
11
State machines 2
Esempio:
F
={i} (stato iniziale)
P = {R,F} (raggiungibilità, essere finale)
A dominio di interpretazione (stati)
12/19/2015
12
State machines 3
Esempi di proprietà:
y R(i, y)
(raggiungibilità)
F(i)
(l’iniziale non è finale)
xyz (R(x, y)  R(x, z)  y=z)
(determinismo)
xy R(x, y) (assenza di deadlock)
12/19/2015
13
State machines 4
In realtà si considera una classe di modelli
(non si specifica totalmente):
 (assertion checking)
se  vale in ogni Mi
(consistency checking)
se  vale in qualche Mi

12/19/2015
14
State machines 5
Fissare la cardinalità degli elementi di
sperando di ottenere un controesempio nel
caso finito
12/19/2015
15
Semantica
12/19/2015
16
Semantica
12/19/2015
17
un tool: Alloy
Uso della logica predicativa e della teoria degli insiemi
12/19/2015
18
Alloy: costruzione di un
controesempio
12/19/2015
19
Alloy: costruzione di un modello
12/19/2015
20