@ FII

Laborator: Small-step SOS

• Back to PLP - Fall 2023

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 prezentate.

Exerciții propuse:

Considerăm cunoscute următoarele definții:

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
| bor : Cond -> Cond -> Cond.
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.

1. (1 punct) Definiți o semantică Small-Step pentru expresiile aritmetice Exp și pentru condițiile Cond din limbajul definit mai sus.

2. (4 puncte) Definiți o semantică Small-Step SOS pentru instrucțiunile din limbajul definit mai sus (1 punct).

   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ță (3 puncte): adăugați la Stmt definit 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/