header "IMP: sintaxis de un lenguaje imperativo simple"
theory Com_b imports BExp_b begin
text{*
Definimos un lenguaje imperativo con las instrucciones básicas
siguientes: asignación, composición secuencial, condicional,
bucle mientras y SKIP (para representar una instrucción sin
ninguna acción a realizar).
Las instrucciones del lenguaje son:
- Assign x e: asignar la expresión aritmética e a la variable x
- Seq c1 c2: realizar la instrucción cs y, a continuación, c2
- If b c1 c2: si la expresión booleana b es verdadera, realiizar c2;
en caso contrario, realizar c2
- While b c: mientras la expresión booleana b sea verdadera,
realizar c.
- SKIP: no hacer nada
*}
text{*
Representamos el lenguaje mediante el siguiente tipo:
*}
datatype
com = SKIP
| Assign vname aexp ("_ ::= _" [1000, 61] 61)
| Seq com com ("_;;/ _" [60, 61] 60)
| If bexp com com ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61)
| While bexp com ("(WHILE _/ DO _)" [0, 61] 61)
text{*
Observaciones:
- Escribiremos Assign x a como x::= e
- Escribiremos Seq c1 c2 como c1 ;; c2
- Escribiremos if b c1 c2 como IF b THEN c1 ELSE c2
- Escribiremos While b c como WHILE b DO c
- La instrucción ;; asocia por la izquierda. Es decir,
c1 ;; c2 ;; c3 es (c1 ;; c2) ;; c3
- Las instrucciones IF y WHILE tienen prelación sobre ;;.
Es decir, WHILE b DO c1 ;; c2 es (WHILE b DO c1) ;; c2.
*}
text{*
Ejemplo:
*}
value "Assign ''y'' (N 2)"
value "''y'' ::= (N 2)"
value "''x'' ::= Plus (V ''y'') (N 1) ;; ''y''::= N 2"
end