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

Exercice : simplification d'expressions

Exercice : compilation d'expressions

Les comparaisons (expressions booléennes)

Les instructions

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.