Definizione di un Linguaggio Formale
Sia C«w¬ =
{(σ,’σ) | B«b¬ σ= true & (σ,σ’) 2 C«w¬ ± C«c¬} [
{(σ,σ) | B«b¬σ = false} =
{(σ,’σ) | B«b¬σ = true & (σ,σ”) 2 C«c¬ & (σ”,σ’) 2 C«w¬} [
{(σ,σ) | B«b¬σ = false}
C«w¬ è una funzione ricorsiva e la sua soluzione è data dal punto fisso di una funzione f(C«w¬) = C«w¬. Tale funzione è definita dal seguente schema di regole
Vedi figura.
(σ, n) 2 A«a¬ , < a, σ > ! n
1. Breve Presentazione del corso
2. Semantica Operazionale del linguaggio imperativo IMP
4. Esercitazione sulla semantica operazionale di IMP e sulle tecniche di prova
5. Definizione Induttiva di Domini
6. Ordinamenti parziali completi, funzioni continue e minimi punti fissi
7. Semantica denotazionale di IMP
8. Semantica denotazionale del comando while di IMP
9. Equivalenza delle semantiche operazionale e denotazionale di Aexp e Bexp di IMP
10. Esercitazione sulle semantiche operazionale e denotazionale di IMP
11. Equivalenza delle semantiche operazionale e denotazionale dei comandi di IMP
12. Esercitazione in aula (sulla prima metà del corso)
13. Linguaggi con Tipi di Ordine Superiori
14. Valutazione Lazy
15. Nondeterminismo e Parallelismo (Concorrenza)
16. Esercitazione in aula sui tipi e sul non-determinismo
17. Communicating Sequential Processes (CSP)
18. Calculus of Communicating Systems (CCS)