diff options
| author | Alex AUVOLAT <alex.auvolat@ens.fr> | 2014-05-07 16:13:31 +0200 |
|---|---|---|
| committer | Alex AUVOLAT <alex.auvolat@ens.fr> | 2014-05-07 16:13:31 +0200 |
| commit | 73fa920959d22c084265fe847f4788564bf49700 (patch) | |
| tree | 9e99d91203b475ebe74fa0b484a86ada05caacf1 /doc/TP1.html | |
| parent | bcde99fbe99174a094f38fdda70ad69d65a423f4 (diff) | |
| download | SemVerif-Projet-73fa920959d22c084265fe847f4788564bf49700.tar.gz SemVerif-Projet-73fa920959d22c084265fe847f4788564bf49700.zip | |
Achieve nothing.
Diffstat (limited to 'doc/TP1.html')
| -rw-r--r-- | doc/TP1.html | 185 |
1 files changed, 185 insertions, 0 deletions
diff --git a/doc/TP1.html b/doc/TP1.html new file mode 100644 index 0000000..dfb8def --- /dev/null +++ b/doc/TP1.html @@ -0,0 +1,185 @@ +<!-- -*- ispell-local-dictionary: "english" -*- --> +<html><head> +<title>Semantics and application to program verification, École normale supérieure, 2013-2014</title> +<meta name="author" content="Antoine Mine"> +<meta http-equiv="Content-Type" content="text/html; charset=UTF-8"> +<link rel="Stylesheet" title="Stylesheet" type="text/css" href="TP1_files/preferred.css"> +<script src="TP1_files/main.js" type="text/javascript"></script> +</head> +<body> + +<h1>Semantics and application to program verification</h1> + +<div id="main"> + +<h2>TP1 - Denotational semantics</h2> + +<p> +The goal of this session is to program an interpreter to compute the denotational semantics of a simple language. +We will use OCaml. + + +</p><h3>Language</h3> + +<p> +Start by downloading the package: <a href="http://www.di.ens.fr/%7Emine/enseignement/l3/codeV1.tgz">codeV1.tgz</a>. + +</p><p> +The package contains a parser for the language, programmed in OCamlLex and Menhir (<tt>lexer.mll</tt> and <tt>parser.mly</tt>). +The parser outputs an abstract syntax tree defined in <tt>abstract_syntax_tree.ml</tt>. +A pretty-printer, to print back an abstract syntax tree into the original language, is provided in <tt>abstract_syntax_printer.ml</tt>. +In <tt>main.ml</tt>, you will find a simple driver that takes a file name passed as argument, parses it, and prints it back. +Just typing <tt>make</tt> should compile the simple driver. + +</p><h4><a name="syntax">Syntax</a></h4> +<p> +The language is a very simple "curly brackets" <tt>C</tt>-like language. +A program is composed of a sequence of statements of the form: +</p><ul> +<li> assignment: <tt>var = expr;</tt> +</li><li> tests: <tt>if (expr) stat-1;</tt> or <tt>if (expr) stat-1; else stat-2;</tt> +</li><li> while loops: <tt>while (expr) stat;</tt> +</li><li> blocks in curly brackets <tt>{ stat-1; ... stat-n; }</tt> +</li></ul> +<p> +non-standard statements include: +</p><ul> +<li> assertions of boolean expressions: <tt>assert (expr);</tt> +</li><li> variable printing: <tt>print (var-1,...,var-n);</tt> +</li><li> failure: <tt>halt;</tt> which stops the program immediately +</li></ul> + +<p> +Expressions include: integer arithmetic operators: <tt>+</tt>, <tt>-</tt>, <tt>*</tt>, <tt>/</tt>, <tt>%</tt> (modulo); boolean operators: <tt>&&</tt> (and), <tt>||</tt> (or), <tt>!</tt> (negation); integer comparisons <tt><</tt>, <tt><=</tt>, <tt>></tt>, <tt>>=</tt>. +Equality <tt>==</tt> and disequality <tt>!=</tt> can be used to compare either two integers or two boolean values. +Constants include integers, and the boolean constants <tt>true</tt> and <tt>false</tt>. +Finally, <tt>rand(l,h)</tt> denotes the non-deterministic interval of integers between the constant <tt>l</tt> and the constant <tt>h</tt>. +You can use <tt>/* ... */</tt> and <tt>//</tt> comments. +You can use parentheses and the operators have their usual precedence. + +</p><p> +Unlike <tt>C</tt>, variables do not need to be declared; they start existing when first assigned a value. +There are no local variables nor functions (see the extension part). + +</p><h4>Semantics</h4> + +<p> +Variables have no type and can hold either an integer or a boolean +value. +Subsequently, we do not distinguish statically between boolean and +integer expressions: only values have a type. +It is an error to use operators with values of the wrong type, such as +adding two boolean values. +This is detected at run-time, when evaluating the expression in the +current environment. +Other run-time errors include: divisions and modulos by zero; using a +non-boolean value in tests, loops and assert conditions; using a +variable that has never been assigned to; asserting a condition that is +false; executing the <tt>halt</tt> statement. + + +</p><h3>Deterministic semantics</h3> + +<p> +We first consider the deterministic subset of the language, i.e., we ignore the <tt>AST_int_rand</tt> expression node for now. + +</p><p> +<b>Write an interpreter that executes the program by induction on the +syntax of statements and expressions; it returns either an environment +mapping variables to values, or an error.</b> + +</p><p> +You can use the following steps: +</p><ol> +<li> Define a type <tt>ival</tt> for values. It should contain integers, + booleans and errors. +You can use a string representation for errors, which will give the user + some information on the location and cause of the error. +To avoid possible overflow in arithmetic, you can use the <tt>ZArith</tt> OCaml library (its API is similar to that of <tt>Int32</tt> and <tt>Int64</tt>; the module is called <tt>Z</tt>). +</li><li> Define a type <tt>env</tt> for environments. You can use the <tt>Map</tt> + functor from the standard OCaml library to represent mappings from +variables to (non-erroneous) values. In addition to such mappings, an <tt>env</tt> object can also represent an error. The initial environment is an empty map (no variable). +</li><li> Write an expression evaluation function <tt>eval_expr: env -> expr ext -> ival</tt> by induction on the syntax of expressions. +It returns an error if its <tt>env</tt> argument is an error +(strictness) or if an error is detected in the expression evaluation, +which then percolates to the expression root. +Avoid using OCaml exceptions to propagate errors in the function: it +will only make the construction of the non-deterministic version more +painful! +</li><li> Write a statement evaluation function <tt>eval_stat: env -> stat ext -> env</tt>. +When should the function return an error environment? +</li><li> +Test your interpreter on the programs from the <tt>examples</tt> directory. +Can you detect infinite loops in <tt>loop.c</tt>, <tt>loop2.c</tt>, and <tt>loop3.c</tt>? +Under which condition does your interpreter terminate? +</li></ol> + +<p class="framed"> +<b>new</b>: correction available in <a href="http://www.di.ens.fr/%7Emine/enseignement/l3/correction/interp_det.ml">interp_det.ml</a>. +(The correction uses abstract syntax trees from the extended language in <a href="http://www.di.ens.fr/%7Emine/enseignement/l3/codeV1x.tgz">codeV1x.tgz</a>) + +</p><h3>Non-deterministic semantics</h3> + +<p> +We now consider the full language including the non-deterministic expression node <tt>rand(l,h)</tt>. + +</p><p> +<b>Write an interpreter for this language that outputs the set of all +possible environments at the end of the program as well as the set of +all errors that can be encountered.</b> + +</p><p> +The structure of the interpreter will be similar to the one in the previous question. +You can use the following steps: +</p><ol> +<li> Define a type <tt>ivalset</tt> to represent sets of values <tt>ival</tt> (including errors). +You can use OCaml's standard <tt>Set</tt> functor. +</li><li> Define a type <tt>envset</tt> to represent sets of environments (including errors). +</li><li> Program a function <tt>eval_expr: env -> expr ext -> ivalset</tt> + to evaluate an expression in a single environment and return the set of + its possible values in the environment. +When encountering a unary node, the operator must be applied to each +possible value of its argument expression; you can use iterators such as + <tt>fold</tt>. +Binary nodes require nested <tt>fold</tt>. +</li><li> Program a filter function <tt>filter: envset -> expr ext -> envset</tt> that returns the subset of its <tt>envset</tt> argument that can satisfy the expression, enriched with the errors encountered during the expression evaluation. +This function will be useful to model loops, tests and assertions. +Remember that an environment can satisfy both an expression and its negation! +</li><li> Program a generic fixpoint operator <tt>fix: ('a -> 'a) -> 'a -> 'a</tt> that iterates a function from a base element to reach a fixpoint. +Use it then in the semantics of loops. +</li><li> +Test your interpreter on the <tt>examples</tt> directory, including non-deterministic programs such as <tt>gcd_nd.c</tt> and <tt>loop4.c</tt>. +</li></ol> + +<p class="framed"> +<b>new</b>: correction available in <a href="http://www.di.ens.fr/%7Emine/enseignement/l3/correction/interp_ndet.ml">interp_ndet.ml</a>. +(The correction uses abstract syntax trees from the extended language in <a href="http://www.di.ens.fr/%7Emine/enseignement/l3/codeV1x.tgz">codeV1x.tgz</a>) + + + +</p><h3>Extensions</h3> + +<p> +You will find in <a href="http://www.di.ens.fr/%7Emine/enseignement/l3/codeV1x.tgz">codeV1x.tgz</a> + an extension of the language with the following additional constructs: +variable declarations (global and local), procedures and functions, <tt>break</tt> and <tt>return</tt> statements, labels and <tt>goto</tt> + statements. +The language is completely backward compatible with the simpler one. +The abstract syntax tree also enriches the previous one with new kinds +of nodes, so that you can simply reuse your interpreter and extend it to + support some or all of the new constructs. + +<br><br> +</p><hr> +<br> +<p> +Author: <a href="http://www.di.ens.fr/%7Emine">Antoine Miné</a> +<br><br> + + +</p></div> + + + + +</body></html>
\ No newline at end of file |