ch9_function_specification/index.html

<html>
<title> Functions and their  specification </title>
<body bgcolor=#08FFFF>
<h1>  Functions and their  specification </h1>
<a href="SRC/chap9.v"> Scripts from the book </a>
<h2> Exercises </h2>
<a href="extract.html"> Exercises 9.1 page 253 and 9.2 page 254  </a> Witness Extraction 
<br> 
<br>   <a href="exo_eqdec.html"> Exercise 9.4 page 254 </a> Equality on nat is decideable 
<br>   <a href="moreperms.html"> Exercise 9.5 page 256 </a> More on permutations 
<br>   <a href="div3.html"> Exercise 9.6 page 270  </a> A three step induction proof 
<br>   <a href="mod2.html"> Exercise 9.7 page 270 </a> A two step induction proof 
<br>   <a href="fib_intro.html"> Exercise 9.8 page 270 </a> The fibonacci sequence 
<br>   <a href="fib_ind.html"> Exercise 9.10 page 271 </a> Reasoning on the fibonacci sequence
<br>   <a href="even_odd.html"> Formal specification of a parity test </a> 
<br>   <a href="div2tofib-ind.html"> Exercise 9.11 page 271 </a> Proofs using specific induction principles

<br>   <a href="div2_mod2.html"> Exercise 9.12 page 270 </a> Euclidean division by 2 
<br>   <a href="plus_prim.html"> Exercise 9.13 page 276 </a> Another addition function 
<br>   <a href="plusss.html"> Exercise 9.14 page 276 </a> Associativity of the tail recursively defined addition 
<br>   <a href="fib_tail.html"> Exercise 9.15 page 276 </a> A tail recursive Fibonacci function 
<br>   <a href="sqrt.html"> Exercise 9.16 page 284 </a> Computing square roots
<br>   <a href="fib_positive.html"> Exercise 9.17 page 284 </a>An efficient Fibonacci function on binary numbers
<br>
<br>
<hr>
<h2> Errata </h2>
<ol>
<li> page 252 (last paragraph of 9.1.1) and page 254 (last paragraph 
of 9.1.2). The old-fashioned syntax of abstraction  : "<tt>[x:A]<em>E</em></tt>"
must be replaced by "<tt>fun x:A => <em>E</em> </tt>"
</ol>


</body>
</html>