Metodi Formali

Semantica Operazionale e Denotazionale

Riassunto gerarchico delle nozioni del corso 2006-2007 di Metodi Formali del Prof. G.M. Pinna - Università degli Studi di Cagliari, Facoltà di Scienze Matematiche Fisiche Naturali, Dipartimento di Matematica ed Informatica, Corso di Laurea Specialistica in Tecnologie Informatiche

  • IMP = Linguaggio Imperativo
    • l'esecuzione di un programma comporta lo svolgimento di una serie di comandi espliciti che ne modificano lo stato
    • N {n, m} numeri interi positivi e negativi
    • T {true, false} valori di verità
    • Loc {X, Y} locazioni
    • Aexp {a} espressioni aritmetiche
      • a ::= n | X | a0 + a1 | a0 - a1 | a0 × a1
    • Bexp {b} espressioni booleane
      • b ::= true | false | a0 = a1 | a0 ≤ a1 | ¬b | b0 ∧ b1 | b0 ∨ b1
    • Com {c} comandi
      • c := skip | X := a | c0 ; c1 | if b then c0 else c1 | while b do c
  • Semantica Operazionale Strutturata
    • insieme di regole che descrivono IMP, che specificano come valutarne le espressioni e come eseguirne i comandi
    • Σ insieme degli stati σ : Loc → N
    • σ(X) contenuto della locazione X nello stato σ
    • σ[m/X] stato ottenuto da σ sostituendo il suo contenuto in X con m;
    • σ[m/X](Y) = {m se Y=X , σ(X) se Y≠X}
    • <a,σ>→n (l'espressione a valutata nello stato σ si riduce al numero n)
    • relazioni di equivalenza
      • b0 ∼ b1 sse ∀t . ∀σ∈Σ . <b0,σ>→t ⇔ <b1,σ>→t
      • c0 ∼ c1 sse ∀σ,σ'∈Σ . <c0,σ>→σ' ⇔ <c1,σ>→σ'
      • c0 ∼ c1 sse ∀σ C[c0]σ = C[c1]σ
      • per verificare l'equivalenza di due funzioni, operazionalmente si confrontano i rispettivi alberi di derivazione, denotazionalmente si cerca uno stato che è presente nell'una ma non nell'altra (controesempio).
    • relazioni di valutazione guidate dalla sintassi
      • premesse / conclusioni
        • (il simbolo "/" va in realtà scritto come una linea orizzontale tra le premesse e le conclusioni)
      • assioma = regola con premesse vuote
        •   / <n,σ>→n
      • Aexp
        • <n,σ>→n (numeri)
        • <X,σ>→σ(X) (locazioni)
        • <a0,σ>→n0 <a1,σ>→n1 / <a0+a1,σ>→n
        • <a0,σ>→n0 <a1,σ>→n1 / <a0-a1,σ>→n
        • <a0,σ>→n0 <a1,σ>→n1 / <a0×a1,σ>→n
      • Bexp
        • <true,σ>→true
        • <false,σ>→false
        • <a0,σ>→n <a1,σ>→m / <a0=a1,σ>→true (n=m)
        • <a0,σ>→n <a1,σ>→m / <a0=a1,σ>→false (n ≠ m)
        • <a0,σ>→n <a1,σ>→m / <a0≤a1,σ>→true (n ≤ m)
        • <a0,σ>→n <a1,σ>→m / <a0≤a1,σ>→false (n > m)
        • <b,σ>→true / <¬b,σ>→false
        • <b,σ>→false / <¬b,σ>→true
        • <b0,σ>→false / <b0∧b1,σ>→false
        • <b0,σ>→true <b1,σ>→false / <b0∧b1,σ>→false
        • <b0,σ>→true <b1,σ>→true / <b0∧b1,σ>→true
        • <b0,σ>→true / <b0∨b1,σ>→true
        • <b0,σ>→false <b1,σ>→true / <b0∨b1,σ>→true
        • <b0,σ>→false <b1,σ>→false / <b0∨b1,σ>→false
      • Com
        • <c,σ>→σ'
        • <skip,σ>→σ
        • <a,σ>→m / <X:=a,σ>→σ[m/X];
        • <c0,σ>→σ" <c1,σ">→σ' / <c0;c1,σ>→σ'
        • <b,σ>→true <c0,σ>→σ' / <if b then c0 else c1,σ>→σ'
        • <b,σ>→false <c1,σ>→σ' / <if b then c0 else c1,σ>→σ'
        • <b,σ>→false / <while b do c,σ>→σ
        • <b,σ>→true <c,σ>→σ" <while b do c,σ">→σ' / <while b do c,σ>→σ'
        • <c,σ>→σ' <b,σ'>→true / <repeat c until b,σ>→σ'
        • <c,σ>→σ' <b,σ'>→false <repeat c until b,σ'>→σ" / <repeat c until b,σ>→σ"
        • 			</ul>
		</li>
	</ul>
</li>
<li>
	Semantica Denotazionale
	<ul>
		<li>
			A : Aexp &rarr; (&Sigma; &rarr; N)
			<ul>
				<li>
					A[n] = {(&sigma;,n) | &sigma;&isin;&Sigma;}
				</li>
				<li>
					A[X] = {(&sigma;,&sigma;(X)) | &sigma;&isin;&Sigma;}
				</li>
				<li>
					A[a<sub>0</sub>+a<sub>1</sub>] = {(&sigma;,n<sub>0</sub>+n<sub>1</sub>) | (&sigma;,n<sub>0</sub>)&isin;A[a<sub>0</sub>] &amp; (&sigma;,n<sub>1</sub>)&isin;A[a<sub>1</sub>]}
				</li>
				<li>
					A[a<sub>0</sub>-a<sub>1</sub>] = {(&sigma;,n<sub>0</sub>-n<sub>1</sub>) | (&sigma;,n<sub>0</sub>)&isin;A[a<sub>0</sub>] &amp; (&sigma;,n<sub>1</sub>)&isin;A[a<sub>1</sub>]}
				</li>
				<li>
					A[a<sub>0</sub>&times;a<sub>1</sub>] = {(&sigma;,n<sub>0</sub>&times;n<sub>1</sub>) | (&sigma;,n<sub>0</sub>)&isin;A[a<sub>0</sub>] &amp; (&sigma;,n<sub>1</sub>)&isin;A[a<sub>1</sub>]}
				</li>
			</ul>
		</li>
		<li>
			B : Bexp &rarr; (&Sigma; &rarr; T)
			<ul>
				<li>
					B[true] = {(&sigma;,true) | &sigma;&isin;&Sigma;}
				</li>
				<li>
					B[false] = {(&sigma;,false) | &sigma;&isin;&Sigma;}
				</li>
				<li>
					B[&not;b] = {(&sigma;,&not;t) | &sigma;&isin;&Sigma; &amp; (&sigma;,t)&isin;B[b]}
				</li>
				<li>
					B[a<sub>0</sub>=a<sub>1</sub>] = {(&sigma;,true) | &sigma;&isin;&Sigma; &amp; A[a<sub>0</sub>]&sigma;=A[a<sub>1</sub>]&sigma;} &cup; {(&sigma;,false) | &sigma;&isin;&Sigma; &amp; A[a<sub>0</sub>]&sigma;&ne;A[a<sub>1</sub>]&sigma;}
				</li>
				<li>
					B[a<sub>0</sub>&le;a<sub>1</sub>] = {(&sigma;,true) | &sigma;&isin;&Sigma; &amp; A[a<sub>0</sub>]&sigma;&le;A[a<sub>1</sub>]&sigma;} &cup; {(&sigma;,false) | &sigma;&isin;&Sigma; &amp; A[a<sub>0</sub>]&sigma;&gt;A[a<sub>1</sub>]&sigma;}
				</li>
				<li>
					B[b<sub>0</sub>&and;b<sub>1</sub>] = {(&sigma;,t<sub>0</sub>&and;t<sub>1</sub>) | &sigma;&isin;&Sigma; &amp; (&sigma;,t<sub>0</sub>)&isin;B[b<sub>0</sub>] &amp; (&sigma;,t<sub>1</sub>)&isin;B[b<sub>1</sub>]}
				</li>
				<li>
					B[b<sub>0</sub>&or;b<sub>1</sub>] = {(&sigma;,t<sub>0</sub>&or;t<sub>1</sub>) | &sigma;&isin;&Sigma; &amp; (&sigma;,t<sub>0</sub>)&isin;B[b<sub>0</sub>] &amp; (&sigma;,t<sub>1</sub>)&isin;B[b<sub>1</sub>]}
				</li>
			</ul>
		</li>
		<li>
			C : Com &rarr; (&Sigma; &rarr; &Sigma;)
			<ul>
				<li>
					C[skip] = {(&sigma;,&sigma;) | &sigma;&isin;&Sigma;}
				</li>
				<li>
					C[X:=a] = {(&sigma;,&sigma;[n/X]) | &sigma;&isin;&Sigma; &amp; n=A[a]&sigma;}
				</li>
				<li>
					C[c<sub>0</sub>;c<sub>1</sub>] = C[c<sub>1</sub>] o C[c<sub>0</sub>] (composizione)
				</li>
				<li>
					C[if b then c<sub>0</sub> else c<sub>1</sub>] = {(&sigma;,&sigma;') | &sigma;,&sigma;'&isin;&Sigma; &amp; B[b]&sigma;=true &amp; (&sigma;,&sigma;')&isin;C[c<sub>0</sub>]} &cup; {(&sigma;,&sigma;') | B[b]&sigma;=false &amp; (&sigma;,&sigma;')&isin;C[c<sub>1</sub>]}
				</li>
				<li>
					C[while b do c] = fix(&Gamma;)<br/>
					&Gamma;(&phi;) = {(&sigma;,&sigma;) | &sigma;,&sigma;'&isin;&Sigma; &amp; B[b]&sigma;=false} &cup; {(&sigma;,&sigma;') | &sigma;,&sigma;'&isin;&Sigma; &amp; B[b]&sigma;=true &amp; (&sigma;,&sigma;')&isin;&phi; o C[c]} 
				</li>
				<li>
					C[repeat c until b] = fix(&Gamma;)<br/>
					&Gamma;(&phi;) = {(&sigma;,&sigma;') | B[b](C[c]&sigma;)=true &amp; (&sigma;,&sigma;')&isin;C[c]} &cup; {(&sigma;,&sigma;') | B[b](C[c]&sigma;)=false &amp; (&sigma;,&sigma;')&isin;&phi; o C[c]}
				</li>
				
			</ul>
		</li>
	</ul>
</li>
<li>
	Equivalenza delle semantiche
	<ul>
		<li>
			&forall;a&isin;Aexp : A[a] = {(&sigma;,n) | &lt;a,&sigma;&gt;&rarr;n}
		</li>
		<li>
			&forall;b&isin;Bexp : B[b] = {(&sigma;,t) | &lt;b,&sigma;&gt;&rarr;t}
		</li>
		<li>
			&forall;c&isin;Com : C[c] = {(&sigma;,&sigma;') | &lt;c,&sigma;&gt;&rarr;&sigma;'}
		</li>
		<li>
			&lt;c,&sigma;&gt;&rarr;&sigma;' &rArr; (&sigma;,&sigma;')&isin;C[c]
		</li>
	</ul>
</li>