Sémantique du langage Niklaus

Niklaus est le langage impératif qui a été utilisé comme exemple dans le cours de traitement des langages. Il est nommé d'après Niklaus Wirth, inventeur du langage Pascal.

Syntaxe de Niklaus

Niklaus est très simple et ne comporte que les concepts suivants :

Un programme a un nom, des variables, et un bloc contenant ses instructions
Un seul type de données, les entiers (équivalent au type int de Java)
Des expressions arithmétiques entières faisant appel au quatre opérations de base avec parenthèses
Des comparaisons d'expressions entières : <, <=, =, <>, >=, et >
Cinq sortes d'instructions :
- read variable, qui lit un entier sur l'entrée standard et stocke sa valeur dans la variable
- write variable, qui écrit la valeur de la variable sur la sortue standard
- L'affectation variable := expression qui range la valeur d'une expression dans une variable
- L'alternative if ( comparaison ) instruction1 else instruction2, qui exécute la première instruction si la comparaison est vraie et la seconde instruction si elle est fausse
- La boucle while ( comparaison instruction, qui exécute une instruction tant qu'une comparaison est vraie.

Par exemple, le programme ci-dessous lit deux entiers sur l'entrée standard, calcule leur PGCD et l'affiche sur la sortie standard :

program pgcd;
var a,b;
{
  read a;
  read b;
  while (a <> b)
  {
    if (a > b) {
      a := a - b;
    } else {
      b := b - a;
    }
  }
  write a;
}

Syntaxe abstraite de Niklaus

Pour donner une sémantique à Niklaus, nous construisons tout d'abord un modèle de sa syntaxe abstraite en Isabelle/HOL.

Les expressions

NikExpressions.thy

theory NikExpressions
imports Main

begin
text ‹
  Niklaus arithmetic expressions.

  An expression may be: 
  ▪ a constant integer value,
  ▪ a variable,
  ▪ the sum, difference, product or quotient of two expressions
›

type_synonym val = ‹int›            ― ‹type of the expression value›
type_synonym varname = ‹string›     ― ‹type of the name of a variable›

text ‹
  For evaluating expressions with variables, we need an environment 
  that tells us the value of the variables. So an environment is
  a function from variable names to values.
›
type_synonym environment = ‹varname ⇒ val›

text ‹Abstract syntax of the expressions in Niklaus (aka meta-model)›
datatype expression =
    Value ‹val›                  (‹N›)                ― ‹so N 2 is the number 2›
  | Variable ‹varname›           (‹V›)                ― ‹so V ''x'' is the variable ''x''›
  | Sum ‹expression› ‹expression›  (infixr ‹.+.› 65)  ― ‹we add dots to avoid confusion with›
  | Diff ‹expression› ‹expression› (infixr ‹.-.› 65)  ― ‹the +, -, * and ÷ predefined operators›
  | Prod ‹expression› ‹expression› (infixr ‹.*.› 75)
  | Quot ‹expression› ‹expression› (infixr ‹.÷.› 75)

text ‹
  Semantics of expressions
  We associate an integer value to an expression in an environment that
  gives the value of variables.
  This semantics is compositional: the semantics of an expression is
  given in terms of the semantics of its parts.
›
fun evaluate:: ‹expression ⇒ environment ⇒ val›
where
    ‹evaluate (N v) env = v›      ― ‹the value of a number is this number›
  | ‹evaluate (V n) env = env n›  ― ‹the value of a variable is given by the environment›
  ― ‹Niklaus arithmetic operations are mapped to the usual operations on integers›
  | ‹evaluate (a .+. b) env = evaluate a env + evaluate b env›
  | ‹evaluate (a .-. b) env = evaluate a env - evaluate b env›
  | ‹evaluate (a .*. b) env = evaluate a env * evaluate b env›
  | ‹evaluate (a .÷. b) env = evaluate a env div evaluate b env›

text ‹A few checks›
value ‹evaluate (N 2 .+. N 3) (λx. 0)›
value ‹evaluate (V ''x'' .+. N 3) ((λu. 0)(''x'':=5))›

end

Exercice : simplification d'expressions

NikExprSimpExercise.thy

theory NikExprSimpExercise

imports NikExpressions

begin
section ‹Simplification of Niklaus arithmetic expressions›

― ‹This is a template to be completed by the students›

text ‹
  Simplifying an expression amounts to replacing:
  ▪ all constant expressions by their value (e.g. N 2 .+. N 3 by N 5)
  ▪ N 0 .+. x and x .+. N 0 by x
  ▪ N 0 .*. x and x .*. N 0 by N 0
  ▪ N 1 .*. x and x .*. N 1 by x
  ▪ N 0 .÷. x by N 0
  ▪ x .÷. N 1 by x
›
fun simplify:: ‹expression ⇒ expression›
where
    ― ‹A binary operator can be simplified if both arguments simplify to numbers›
    ‹simplify (a .+. b) = (
       let (u', v') = (simplify a, simplify b) in
       if u' = (N 0) then v'
       else if v' = (N 0) then u'
       else
       case (u', v') of
           (N va, N vb) ⇒ N (va + vb)  ― ‹arguments are numbers ⇒ compute the result›
         | (sa, sb) ⇒ sa .+. sb        ― ‹else return the sum of the simplified arguments›
    )›
  | ‹simplify (a .-. b) = (
       let (u', v') = (simplify a, simplify b) in
         u' .-. v' ― ‹FIX ME: this is just a place holder›
    )›
  ― ‹Other cases ...›

  ― ‹Default: variables and constants cannot be simplified and are left as is›
  | ‹simplify expr = expr›

text ‹Some checks›
value ‹simplify ((N 2) .*. (N 3))›
value ‹simplify (N 2 .*. N 1 .+. V ''x'')›
value ‹simplify (N 0 .*. (N 1 .+. V ''x''))›
value ‹simplify ((N 2 .-. N 2) .*. (N 1 .+. V ''x''))›

text ‹Proof that simplify does not change the semantics of expressions›
theorem ‹evaluate (simplify expr) env = evaluate expr env›
― ‹
  Hint: there is a theorem @{thm expression.split} that splits a proof on expressions
  into smaller proofs on the different kinds of expressions.
  You can use it with simp, the syntax is "apply (simp split: expression.split)".
  This also works with "auto".
›
sorry

text ‹
  A predicate telling whether an expression is optimal, i.e. does not
  contain any operator applied to constants.
›
fun optimal_expr :: ‹expression ⇒ bool›
where
    ‹optimal_expr (N a) = True›
  | ‹optimal_expr (V x) = True›
  ― ‹Other cases... ›

text ‹Check that optimal_expr behaves as expected›
value ‹optimal_expr (N 3)›
value ‹optimal_expr (N 3 .+. V ''x'')›
value ‹optimal_expr (N 0 .+. V ''x'')›
value ‹optimal_expr (N 3 .+. N 5)›
value ‹optimal_expr ((N 3 .+. V ''x'') .*. V ''y'')›
value ‹optimal_expr ((N 3 .+. N 2) .*. V ''y'')›
value ‹optimal_expr (N 0 .*. V ''x'')›

text ‹Prove that simplify yields optimal expressions›
theorem ‹optimal_expr (simplify expr)›
― ‹
  Hint: since the simplification of an operator depends on the form of
  the simplification of its arguments, we have to analyse the different
  cases. This can be done using the "case_tac" tactic.
  For instance, to analyse all the cases for expression e, we
  can use "apply (case_tac ‹e›)", and then process each case.
›
sorry

end

Exercice : compilation d'expressions

NikExprCompileExercise.thy

theory NikExprCompileExercise

imports NikExpressions

begin

section ‹Compilation of Niklaus arithmetic expressions›

text ‹
  We compile Niklaus arithmetic expressions toward the instruction set of a stack processor 
  with five instructions:
  ▪ PUSH i, that pushed the integer value i onto the stack
  ▪ ADD, that replaces the top two integers on the stack by their sum
  ▪ SUB, that replaces the top two integers on the stack by their difference
  ▪ MUL, that replaces the top two integers on the stack by their product
  ▪ DIV, that replaces the top two integers on the stack by their Euclidian quotient
›
text ‹Target arithmetic instruction set›
datatype Instruction = 
  PUSH int
| ADD
| SUB
| MUL
| DIV

text ‹
  The instructions operate on a stack of integers that we represent as a list, 
  the first item being the top of the stack.
›
type_synonym data_stack=‹int list›

text ‹Executing an arithmetic instruction modifies the stack›
fun exec::‹Instruction ⇒ data_stack ⇒ data_stack›
where
  ‹exec (PUSH i) stack = ― ‹FIX ME› undefined›
| ‹exec ADD (a#b#stack) = ― ‹FIX ME› undefined›
| ‹exec SUB (a#b#stack) = ― ‹FIX ME› undefined›
| ‹exec MUL (a#b#stack) = ― ‹FIX ME› undefined›
| ‹exec DIV (a#b#stack) = ― ‹FIX ME› undefined›
| ‹exec _ stack = ― ‹FIX ME› undefined›

text ‹A program is a list of instructions›
type_synonym Program=‹Instruction list›

text ‹Executing a program modifies the stack›
primrec execute::‹Program ⇒ data_stack ⇒ data_stack›
where
  ‹execute [] stack = ― ‹FIX ME› undefined›
| ‹execute (op#l) stack = ― ‹FIX ME› undefined›

text ‹
  Compiling an expression into a program produces a list of instructions 
  that push the values on the stack and compute the result. An environment
  is needed to know the value of variables in the expression.
›
primrec compile::‹expression ⇒ environment ⇒ Program›
where
  ‹compile (N i) env = ― ‹FIX ME› undefined›
| ‹compile (V x) env = ― ‹FIX ME› undefined›
| ‹compile (e1 .+. e2) env = ― ‹FIX ME› undefined›
| ‹compile (e1 .-. e2) env = ― ‹FIX ME› undefined›
| ‹compile (e1 .*. e2) env = ― ‹FIX ME› undefined›
| ‹compile (e1 .÷. e2) env = ― ‹FIX ME› undefined›

text ‹Some checks›
abbreviation ‹expr_1 ≡ V ''x'' .-. N 2›
abbreviation ‹env_1 ≡ (λv. 0)(''x'':=5)›
value ‹evaluate expr_1 env_1›
value ‹compile expr_1 env_1›
value ‹execute (compile expr_1 env_1) []›

subsection ‹Proving the correctness of the compiler›

text ‹
  The compiler is correct: executing the compiled code of an expression 
  gives the same value as evaluating the expression
›
theorem ‹execute (compile expr env) stack = ― ‹FIX ME› undefined›
sorry

end

Pour cet exercice, il vous sera utile de consulter la preuve de correction que j'ai faite à la suite de
l'épisode Program correctness de la chaîne Youtube Computerphile.

Les comparaisons (expressions booléennes)

NikBoolExpr.thy

theory NikBoolExpr
imports NikExpressions

begin

section ‹
  Niklaus boolean expressions (conditions for if and while)
›

text ‹
  A boolean expression may consist in the comparison
  of two arithmetic expressions, or in a boolean value
›
datatype boolexp = 
    Equals expression expression       (infix ".=." 55)
  | Differs expression expression      (infix ".≠." 55)
  | LowerThan expression expression    (infix ".<." 55)
  | LowerEqual expression expression   (infix ".≤." 55)
  | GreaterThan expression expression  (infix ".>." 55)
  | GreaterEqual expression expression (infix ".≥." 55)
  | Boolean bool                       ("B")

text ‹Semantics of boolean expressions is mapped to the usual operators on integers›
fun evalbool :: "boolexp ⇒ environment ⇒ bool"
where
    "evalbool (e1 .=. e2) env =  (evaluate e1 env = evaluate e2 env)"
 |  "evalbool (e1 .≠. e2) env =  (evaluate e1 env ≠ evaluate e2 env)"
 |  "evalbool (e1 .<. e2) env =  (evaluate e1 env < evaluate e2 env)"
 |  "evalbool (e1 .≤. e2) env =  (evaluate e1 env ≤ evaluate e2 env)"
 |  "evalbool (e1 .>. e2) env =  (evaluate e1 env > evaluate e2 env)"
 |  "evalbool (e1 .≥. e2) env =  (evaluate e1 env ≥ evaluate e2 env)"
 |  "evalbool (B b) env = b"

text ‹Checks on some expressions›
value "evalbool (N 2 .+. V ''x'' .=. N 4) ((λx.0)(''x'':=5))"
value "evalbool (N 2 .+. V ''x'' .=. N 4)  ((λx.0)(''x'':=2))"
value "evalbool (B True) (λx. 0)"

end

Les instructions

NikInstructions.thy

theory NikInstructions
imports NikExpressions NikBoolExpr

begin
section ‹Abstract syntax of the instructions in Niklaus›

text ‹
  Without the Read and Write instructions, the state 
  of the Niklaus execution machine is reduced to the
  environment (valuation of the variables)
›
type_synonym state = "environment"

text ‹
  Instructions are:
  ▪ Nop, does nothing, useful for if _ then _ else when a branch is empty
  ▪ VarDecl v (abbreviated into "var v"), declares a variable (initial value is 0)
  ▪ Seq i1 i2 (abbreviated as "i1;; i2) executes i1 and i2 in sequence
  ▪ Alternative c i1 i2 ("if c then i1 else i2 fi"), executes i1 if c is true, else executes i2
  ▪ While c body ("while c do body done"), executes body if c is true, then executes itself again
›
datatype instruction = 
    Nop
  | VarDecl varname                ("var")
  | Assign varname expression      ("_ <- _" [1000, 65] 65)
  | Seq instruction instruction    ("_ ;; _" [65, 60] 60)
  | Alternative boolexp instruction instruction
                                   ("if _ then _ else _ fi")
  | While boolexp instruction      ("while _ do _ done")

text ‹Check that we can write some simple instructions with this syntax›
term "var ''x''"
term "if V ''x'' .<. N 2 then ''x'' <- N 2 else ''x''<- V ''x'' .-. N 1 fi"

end

Sémantique opérationnelle de Niklaus

Nous définissons la sémantique opérationnelle à grand pas de Niklaus comme une relation {$\leadsto$} entre une paire (instruction, état) et des états. {$(i, s) \leadsto s'$} si et seulement si l'exécution de {$i$} dans l'état {$s$} peut mener à l'état {$s'$}.

Sémantique dénotationnelle de Niklaus

Nous définissons la sémantique dénotationnelle de Niklaus comme une fonction {$⟦\,\_\,⟧$} qui à chaque instruction associe une relation entre états. {$(s, s') \in ⟦\,i\,⟧$} si et seulement si on peut passer de l'état {$s$} à l'état {$s'$} en exécutant {$i$}.

Sémantique axiomatique de Niklaus

Nous définissons la sémantique axiomatique de Niklaus comme un ensemble de règles de déduction qui permettent de raisonner sur les pré et les post-conditions d'un programme. Nous montrons la correction de ce système de déduction par rapport à la sémantique opérationnelle, et nous montrons également sa complétude en introduisant la notion de plus faible précondition.