@ FII

Laborator 6: Evaluarea programelor imperative simple

Back to PLP - Fall 2023

Exerciții de antrenament:

Definiți un environment Env de tip string -> nat și o funcție update care actualizează valoarea unei variable de tip string cu o valoare de tipul nat. Testați funcția update pe câteva exemple.
Consultați tipul option din documentația oficială. Citiți cu atenție definiția tipului.

Exerciții propuse:

(1 punct) Definiți un interpretor pentru expresiile aritmetice definite mai jos:

Inductive AExp :=
| num : nat -> AExp
| var : string -> AExp
| add : AExp -> AExp -> AExp
| sub : AExp -> AExp -> AExp
| div : AExp -> AExp -> AExp.

Atenție la operațiile de scădere și împărțire: acestea pot produce erori. De aceea, un evaluator pentru expresii aritmetice va returna tipul option nat în loc de nat. Pentru detalii despre option puteți rula pe rând comenzile:

Check option.
Check option nat.
Print option.
Check (Some 2).
Check None.

(1 punct) Definiți un interpretor pentru limbajul de definit în laboratorul anterior (a cărui sintaxa abstractă pentru expresii booleene și instrucțiuni este amintită mai jos). După definirea interpretorului, testați programele care (1) calculează cel mai mare divizor comun a două numere (Euclid cu scăderi repetate) și (2) cel care calculează cel de-al n-lea termen al șirului Fibonacci.

Inductive Cond :=
| base : bool -> Cond
| bnot : Cond -> Cond
| beq  : AExp -> AExp -> Cond
| less : AExp -> AExp -> Cond
| band : Cond -> Cond -> Cond.
Inductive Stmt :=
| skip : Stmt 
| assign : string -> Exp -> Stmt
| seq : Stmt -> Stmt -> Stmt
| ite : Cond -> Stmt -> Stmt -> Stmt (* if-then-else *)
| while : Cond -> Stmt -> Stmt.

Atenție: operațiile pentru expresii aritmetice va returna tipul option nat în loc de nat. Acest lucru are impact asupra rezultatului interpretării expresiilor booleene.

(3 puncte) Definiți un interpretor pentru logica propozițională. Detalii sunt disponibile aici: [Logica propozițională]. Se acordă 1 punct pentru definirea corectă a sintaxei, 1 punct pentru definirea asignărilor și a unor exemple de asignări, și 1 punct pentru semantică și exemple care ilustrează funcționarea corectă.

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