@ FII

Laborator 7

• Back to PLP - Fall 2022
• Small-step SOS

Exerciții de antrenament:

• Citiți cu atenție semantica Small-step SOS a limbajului IMP discutată la curs. Rulați din nou exemplele și demonstrațiile discutate.

Exerciții propuse:

1. (2p) Definiți o semantică Small-step pentru expresiile (aritmetice și booleene) definite mai jos și scrieți câte un exemplu simplu de derivare pentru fiecare tip de expresie:

Inductive Exp :=
| num : nat -> Exp
| var : string -> Exp
| add : Exp -> Exp -> Exp
| sub : Exp -> Exp -> Exp
| div : Exp -> Exp -> Exp.
Inductive Cond :=
| base : bool -> Cond
| bnot : Cond -> Cond
| beq  : Exp -> Exp -> Cond
| less : Exp -> Exp -> Cond
| band : Cond -> Cond -> Cond.

Nat.sub și Nat.div (din modulul Nat predefinite în Coq) pot fi utilizate pentru operațiile de scădere și înmulțire.

2. (3p) Definiți o semantică Small-step SOS pentru instrucțiunile definite mai jos și scrieți câte un exemplu simplu de derivare pentru fiecare instrucțiune:

Inductive Stmt :=
| skip : Stmt
| assign : string -> Exp -> Stmt
| seq : Stmt -> Stmt -> Stmt
| ite : Cond -> Stmt -> Stmt -> Stmt (* if-then-else *)
| it  : Cond -> Stmt -> Stmt (* if-then *)
| dowhile : Stmt -> Cond -> Stmt.

3. Bonus (10 puncte) La adresa https://softwarefoundations.cis.upenn.edu/plf-current/Smallstep.html#lab176 se găsește o implementare pentru un limbaj concurent numit Concurrent IMP. Acest limbaj conține o instrucțiune care se numește CPar ce permite executarea în paralel a două instrucțiuni. Cerință: adăugați la Stmt definit la exercițiul 2 instrucțiunea CPar și apoi demonstrați o proprietate similară cu cea din exercițiul https://softwarefoundations.cis.upenn.edu/plf-current/Smallstep.html#lab178.

Coq Reference Manual: https://coq.inria.fr/distrib/current/refman/