Práctica 6 (3/11): intérpretes

---

Explicación lab 3

Repo de hoy: https://github.com/compiladores/esqueleto-jsonlang

Brevísimo resumen de semánticas formales

• Semántica axiomática (Lógica de Hoare): expresa la semántica por medio de pre y post condiciones
• Semántica operacional: como la axiomática pero con más conceptos, que modelan conceptos como la RAM, programas posibles, etc. como conjuntos.
• Semántica denotacional: Interpreta el programa como una función matemática que involucra la RAM, contextos, etc.

---

Triplas de Hoare

$$\{P\}C\{Q\}$$

Al ejecutar $C$, si el estado del programa es $P$, pasa a ser $Q$

Ejemplo

Asignación en C

$$\{S\} \texttt{ int x = 4; } \{S \land x=4\}$$

$$\{S\} \texttt{ int x = $N$; } \{S \land x=N\}$$

Secuencia:

$$\{A\} \texttt{$S_1$} \{B\}, \{B\} \texttt{$S_2$} \{C\} \Rightarrow \{A\} \texttt{$S_1$;$S_2$} \{C\}$$

---

Semántica Denotacional

Cada construcción sintáctica del programa se convierte en una representación matemática rigurosa de lo que hace.

Ejemplo

En C, todo el código que puede ejecutarse es un statement, así, podemos tener:

• if statement
• while statement
• block statement
• assign statement
• expression statement

Una función semántica va a ser será una $F: Statement \to (RAM \times disk \to RAM \times disk)$

---

Jsonlang: un lenguaje de POJOs

• $J$: valores javascript válidos
• $expr\subset J$: expresiones del lenguaje
• $C:string\to J$: diccionario contexto
• $S:\N\to J$: lista
• $S_i\subset S$ inputs, $S_o\subset S$ outputs

Sea la función semántica:

$$F:expr \times D \times S_i \times S_o\to J \times D \times S_i \times S_o$$

Esta función semántica vamos a llamarla eval. Ejemplos en el código.

---

Ejercício

Agregarle algo de lo siguiente a Jsonlang. La función semántica debe mantenerse funcional:

• un if
• un while
• un for
• scopes
• funciones