@ FII

Laborator: Big-step SOS

• Back to PLP - Fall 2023

Exerciții de antrenament:

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

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ă Big-step pentru expresiile aritmetice din limbajul definit mai sus. Scrieți cel puțin câte două teste pentru fiecare dintre operațiile sub și div: atenție la cazurile de eroare.

   Se acordă 0.5 puncte pentru tratarea corectă a scăderii sub și 0.5 puncte pentru tratarea corectă a împărțirii div.

2. (1.5 puncte) Definiți o semantică Big-step pentru condiții (Cond) din limbajul definit mai sus, astfel:

   1. evaluare secvențială pentru less, astfel încât primul argument să fie redus mai întâi (0.5 puncte);
   2. evaluare parțială pentru bor, astfel încât, dacă primul argument este true, atunci nu mai trebuie redus și al doilea argument (0.5 puncte);
   3. evaluarea ambelor argumente concomitent pentru beq (0.5 puncte).

3. (2.5 puncte) Definiți o semantică Big-step SOS pentru instrucțiunile din limbajul definit mai sus și scrieți câte un exemplu simplu de derivare pentru fiecare instrucțiune.

   Se acordă câte 0.5 puncte pentru fiecare instrucțiune tratată corect și însoțită de teste.

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