quick headers to put VSTTE'10 solutions online

419c40e8 · Jean-Christophe Filliâtre · 9ac18bf3 · 419c40e8 · 419c40e8 · 419c40e8
Commit 419c40e8 authored Jun 22, 2011 by Jean-Christophe Filliâtre
5 changed files
--- a/examples/programs/vstte10_aqueue.mlw
+++ b/examples/programs/vstte10_aqueue.mlw
-(* VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
-   Problem 5: amortized queue *)
+(*
+   VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
+   Problem 5: amortized queue
+
+   Author: Jean-Christophe Filliâtre (CNRS)
+   Tool:   Why3 (see https://gforge.inria.fr/projects/why3/)
+*)

 module AmortizedQueue


--- a/examples/programs/vstte10_inverting.mlw
+++ b/examples/programs/vstte10_inverting.mlw
-(* VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
-   Problem 2: inverting an injection *)
+(*
+   VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
+   Problem 2: inverting an injection
+
+   Author: Jean-Christophe Filliâtre (CNRS)
+   Tool:   Why3 (see https://gforge.inria.fr/projects/why3/)
+*)

 module InvertingAnInjection


--- a/examples/programs/vstte10_max_sum.mlw
+++ b/examples/programs/vstte10_max_sum.mlw
-(* VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
-   Problem 1: maximum and sum of an array *)
+(*
+   VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
+   Problem 1: maximum and sum of an array
+
+   Author: Jean-Christophe Filliâtre (CNRS)
+   Tool:   Why3 (see https://gforge.inria.fr/projects/why3/)
+*)

 module MaxAndSum


--- a/examples/programs/vstte10_queens.mlw
+++ b/examples/programs/vstte10_queens.mlw
-(* VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
-   Problem 4: N-queens *)
+(*
+   VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
+   Problem 4: N-queens
+
+   Author: Jean-Christophe Filliâtre (CNRS)
+   Tool:   Why3 (see https://gforge.inria.fr/projects/why3/)
+*)

 module NQueens


--- a/examples/programs/vstte10_search_list.mlw
+++ b/examples/programs/vstte10_search_list.mlw
-(* VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
-   Problem 3: searching a linked list *)
+(*
+   VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
+   Problem 3: searching a linked list
+
+   Author: Jean-Christophe Filliâtre (CNRS)
+   Tool:   Why3 (see https://gforge.inria.fr/projects/why3/)
+*)

 module SearchingALinkedList