Skip to content

why3
why3
Commit cf1b77f1 authored by Jean-Christophe Filliatre's avatar Jean-Christophe Filliatre
Browse files
Options

cleaning up examples for the gallery

parent 46bc918d
Hide whitespace changes
Inline Side-by-side
Showing with 211 additions and 38 deletions
Makefile.in
View file @ cf1b77f1
......@@ -348,21 +348,22 @@ install_local: bin/why3ml
# gallery
##########
GALLERYPGMS = binary_search bresenham sf same_fringe relabel quicksort \
power mergesort_list mac_carthy isqrt insertion_sort_list flag \
distance muller fib_memo fibonacci \
vstte10_aqueue vstte10_inverting vstte10_max_sum \
vstte10_queens vstte10_search_list \
vacid_0_sparse_array
# we export exactly the programs that have a why3session.xml file
.PHONY: gallery
gallery::
@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
@for f in $(GALLERYPGMS); do \
@for x in `find examples/programs/ -name why3session.xml`; do \
d=`dirname $$x`; \
f=`basename $$d`; \
echo "exporting $$f"; \
mkdir -p $(GALLERYDIR)/$$f; \
cp examples/programs/$$f.mlw $(GALLERYDIR)/$$f/; \
rm -f $(GALLERYDIR)/$$f/$$f.zip; \
cd examples/programs/; \
zip -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f; \
cd ../..; \
done
########
......
examples/programs/bresenham/why3session.xml 0 → 100644
View file @ cf1b77f1
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/bresenham/why3session.xml">
<file name="../bresenham.mlw" verified="false" expanded="true">
<theory name="WP M" verified="false" expanded="true">
<goal name="Invariant_is_ok" sum="390f64d8a0d8118b5ecd73b966e91e83" proved="false" expanded="true">
</goal>
<goal name="WP_parameter bresenham" expl="correctness of parameter bresenham" sum="6d68a3113e31069fe7080c7ab2bfdb70" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter bresenham.1" expl="loop invariant init" sum="37b77c77cba7d3b5f341f0e4f308cb16" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter bresenham.2" expl="assertion" sum="261b58b58e5e484e392100c7ae9d46de" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.28"/>
</proof>
</goal>
<goal name="WP_parameter bresenham.3" expl="loop invariant preservation" sum="759d37f0de1364d96fb2692fd67ebb58" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter bresenham.4" expl="loop variant decreases" sum="59657e5a7dd65c09ea874478e0b9dece" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter bresenham.5" expl="loop invariant preservation" sum="770bc300939ef2bcd62424a5d711ad03" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="WP_parameter bresenham.6" expl="loop variant decreases" sum="37037d827452040cc8d6b2b51285c2a2" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter bresenham.7" expl="normal postcondition" sum="7ac7b0b6bcb369354660f76821cacb1a" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
examples/programs/fib_memo/why3session.xml 0 → 100644
View file @ cf1b77f1
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/fib_memo/why3session.xml">
<file name="../fib_memo.mlw" verified="true" expanded="true">
<theory name="WP M" verified="true" expanded="true">
<goal name="WP_parameter fibo" expl="correctness of parameter fibo" sum="75546b1b867d7e220a43a0f9c16568a2" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter memo_fibo" expl="correctness of parameter memo_fibo" sum="743b19a4394b2b79b9ef838a624045c7" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter memo_fibo.1" expl="normal postcondition" sum="935d25dee5b707cf0bd087e131e709da" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter memo_fibo.2" expl="precondition" sum="2efb9e3e13eeb740e06fe133ea0ed5da" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter memo_fibo.3" expl="normal postcondition" sum="12383032cf9410a6d7547ff592884006" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
examples/programs/gcd.mlw
View file @ cf1b77f1
module M
(* Greatest common divisor, using the Euclidean algorithm *)
module EuclideanAlgorithm
use import int.Int
use import int.Gcd
......
examples/programs/gcd/why3session.xml
View file @ cf1b77f1
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/gcd/why3session.xml">
<file name="../gcd.mlw" verified="false" expanded="true">
<theory name="WP M" verified="false" expanded="true">
<goal name="WP_parameter gcd" expl="correctness of parameter gcd" sum="13686aa7223ccd074e11892070fa497c" proved="false" expanded="true">
<transf name="split_goal" proved="false" expanded="true">
<goal name="WP_parameter gcd.1" expl="normal postcondition" sum="e04458a1deb8f46c32e2040984924ab2" proved="true" expanded="true">
<file name="../gcd.mlw" verified="true" expanded="true">
<theory name="WP EuclideanAlgorithm" verified="true" expanded="true">
<goal name="WP_parameter gcd" expl="correctness of parameter gcd" sum="bfbae7b37de6ad9ac15a7666cdb75bce" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter gcd.1" expl="normal postcondition" sum="3893c6278b0c6d2e8a61ff8df2953fcb" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
......@@ -16,15 +16,15 @@
<result status="valid" time="0.00"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.65"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter gcd.2" expl="precondition" sum="b1c7e0b73a7e08e9bfb9e73aa85762d7" proved="true" expanded="true">
<goal name="WP_parameter gcd.2" expl="precondition" sum="af7096cc1cd7bdcb9f88d52ad341c488" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.06"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.00"/>
......@@ -33,18 +33,9 @@
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter gcd.3" expl="normal postcondition" sum="c0a0f540fca852dd68a554221754e076" proved="false" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="1.08"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.48"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.09"/>
</proof>
<goal name="WP_parameter gcd.3" expl="normal postcondition" sum="9ac7a295784dbed7c5dfdb55575495d7" proved="true" expanded="true">
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.09"/>
<result status="valid" time="6.84"/>
</proof>
</goal>
</transf>
......
examples/programs/muller/why3session.xml 0 → 100644
View file @ cf1b77f1
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/muller/why3session.xml">
<file name="../muller.mlw" verified="true" expanded="true">
<theory name="WP Muller" verified="true" expanded="true">
<goal name="WP_parameter compact" expl="correctness of parameter compact" sum="4c063005b5cf1e6f759d13f120345d04" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter compact.1" expl="for loop initialization" sum="dd0305a2f1fce9b990ae437ad6329b29" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter compact.2" expl="for loop preservation" sum="2b9da44da537e6c7c27e61d1c836bf6a" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter compact.3" expl="for loop initialization" sum="c0e3d5971e572acd3db62fb9e102a17c" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter compact.4" expl="for loop preservation" sum="29d3a6379052aaea805d7c00bf87fccf" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.06"/>
</proof>
</goal>
<goal name="WP_parameter compact.5" expl="for loop initialization" sum="a2e57724df2cb5bae002bfdde74ecae8" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.08"/>
</proof>
</goal>
<goal name="WP_parameter compact.6" expl="for loop preservation" sum="d08e9f45a079dc2f15abdefb952805c9" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.14"/>
</proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
examples/programs/sf/why3session.xml 0 → 100644
View file @ cf1b77f1
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/sf/why3session.xml">
<file name="../sf.mlw" verified="true" expanded="true">
<theory name="WP HoareLogic" verified="true" expanded="true">
<goal name="WP_parameter slow_subtraction" expl="correctness of parameter slow_subtraction" sum="458f2e6c9d1bbc6a9d6cdddba40fd1d5" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter reduce_to_zero" expl="correctness of parameter reduce_to_zero" sum="45e7a1303fcca8e459e15eca9d92bccd" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter slow_addition" expl="correctness of parameter slow_addition" sum="f19498eb4d9626d1453e5ecf3f3f0abc" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="even_not_odd" sum="53e6bf87df0a78f77396dc37febf9ad4" proved="true" expanded="true">
<proof prover="coq" timelimit="10" edited="sf_WP_HoareLogic_even_not_odd_1.v" obsolete="false">
<result status="valid" time="0.65"/>
</proof>
</goal>
<goal name="WP_parameter parity" expl="correctness of parameter parity" sum="f6d9f277eb9aef02765d7c85c0442161" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.13"/>
</proof>
</goal>
<goal name="WP_parameter sqrt" expl="correctness of parameter sqrt" sum="cf2cff74151b7962afd722bedeef6915" proved="true" expanded="true">
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter factorial" expl="correctness of parameter factorial" sum="9ea847303a87e605060c175e0d0e09e4" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
</theory>
<theory name="WP MoreHoareLogic" verified="true" expanded="true">
<goal name="WP_parameter list_sum" expl="correctness of parameter list_sum" sum="3e6044f1b8cf49c626655c2cd6cc12a0" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.08"/>
</proof>
</goal>
<goal name="WP_parameter list_member" expl="correctness of parameter list_member" sum="5f5617227f186b821f84ef28ca6c0dbd" proved="true" expanded="true">
<proof prover="yices" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.09"/>
</proof>
</goal>
</theory>
</file>
</why3session>
examples/programs/vstte10_aqueue.mlw
View file @ cf1b77f1
......@@ -2,8 +2,8 @@
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/)
Author: Jean-Christophe Filliatre (CNRS)
Tool: Why3 (see http://why3.lri.fr/)
*)
module AmortizedQueue
......
examples/programs/vstte10_inverting.mlw
View file @ cf1b77f1
......@@ -2,8 +2,8 @@
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/)
Author: Jean-Christophe Filliatre (CNRS)
Tool: Why3 (see http://why3.lri.fr/)
*)
module InvertingAnInjection
......
examples/programs/vstte10_max_sum.mlw
View file @ cf1b77f1
......@@ -2,8 +2,8 @@
VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
Problem 1: maximum /\ sum of an array
Author: Jean-Christophe Filliâtre (CNRS)
Tool: Why3 (see https://gforge.inria.fr/projects/why3/)
Author: Jean-Christophe Filliatre (CNRS)
Tool: Why3 (see http://why3.lri.fr/)
*)
module MaxAndSum
......
examples/programs/vstte10_queens.mlw
View file @ cf1b77f1
......@@ -2,8 +2,8 @@
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/)
Author: Jean-Christophe Filliatre (CNRS)
Tool: Why3 (see http://why3.lri.fr/)
*)
module NQueens
......
examples/programs/vstte10_search_list.mlw
View file @ cf1b77f1
......@@ -2,8 +2,8 @@
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/)
Author: Jean-Christophe Filliatre (CNRS)
Tool: Why3 (see http://why3.lri.fr/)
*)
module SearchingALinkedList
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment