Insertion Sort, naive version, Coq proofs for hard cases

6585b235 · MARCHE Claude · 7e0134b6 · 6585b235 · 6585b235 · 6585b235
Commit 6585b235 authored Feb 07, 2013 by MARCHE Claude
--- a/examples/hoare_logic/blocking_semantics.mlw
+++ b/examples/hoare_logic/blocking_semantics.mlw
--- a/examples/hoare_logic/blocking_semantics/blocking_semantics_WP_progress_1.v
+++ b/examples/hoare_logic/blocking_semantics/blocking_semantics_WP_progress_1.v
--- a/examples/hoare_logic/blocking_semantics/blocking_semantics_WP_wp_conj_1.v
+++ b/examples/hoare_logic/blocking_semantics/blocking_semantics_WP_wp_conj_1.v
--- a/examples/hoare_logic/blocking_semantics/blocking_semantics_WP_wp_reduction_1.v
+++ b/examples/hoare_logic/blocking_semantics/blocking_semantics_WP_wp_reduction_1.v
--- a/examples/hoare_logic/blocking_semantics2.mlw
+++ b/examples/hoare_logic/blocking_semantics2.mlw
--- a/examples/hoare_logic/blocking_semantics2/blocking_semantics2_WP_bool_value_1.v
+++ b/examples/hoare_logic/blocking_semantics2/blocking_semantics2_WP_bool_value_1.v
--- a/examples/hoare_logic/blocking_semantics2/blocking_semantics2_WP_bool_value_2.v
+++ b/examples/hoare_logic/blocking_semantics2/blocking_semantics2_WP_bool_value_2.v
--- a/examples/hoare_logic/blocking_semantics2/blocking_semantics2_WP_distib_conj_1.v
+++ b/examples/hoare_logic/blocking_semantics2/blocking_semantics2_WP_distib_conj_1.v
--- a/examples/hoare_logic/blocking_semantics2/blocking_semantics2_WP_monotonicite_1.v
+++ b/examples/hoare_logic/blocking_semantics2/blocking_semantics2_WP_monotonicite_1.v
--- a/examples/hoare_logic/blocking_semantics2/blocking_semantics2_WP_monotonicity_1.v
+++ b/examples/hoare_logic/blocking_semantics2/blocking_semantics2_WP_monotonicity_1.v
--- a/examples/hoare_logic/blocking_semantics2/blocking_semantics2_WP_progress_1.v
+++ b/examples/hoare_logic/blocking_semantics2/blocking_semantics2_WP_progress_1.v
--- a/examples/hoare_logic/blocking_semantics2/blocking_semantics2_WP_result_always_fresh_in_wp_1.v
+++ b/examples/hoare_logic/blocking_semantics2/blocking_semantics2_WP_result_always_fresh_in_wp_1.v
--- a/examples/hoare_logic/blocking_semantics2/blocking_semantics2_WP_unit_value_1.v
+++ b/examples/hoare_logic/blocking_semantics2/blocking_semantics2_WP_unit_value_1.v
--- a/examples/hoare_logic/blocking_semantics2/blocking_semantics2_WP_wp_implies_1.v
+++ b/examples/hoare_logic/blocking_semantics2/blocking_semantics2_WP_wp_implies_1.v
--- a/examples/hoare_logic/blocking_semantics2/blocking_semantics2_WP_wp_reduction_1.v
+++ b/examples/hoare_logic/blocking_semantics2/blocking_semantics2_WP_wp_reduction_1.v
--- a/examples/hoare_logic/blocking_semantics2/blocking_semantics2_WP_wp_reduction_2.v
+++ b/examples/hoare_logic/blocking_semantics2/blocking_semantics2_WP_wp_reduction_2.v
--- a/examples/hoare_logic/blocking_semantics2/why3session.xml
+++ b/examples/hoare_logic/blocking_semantics2/why3session.xml
--- a/examples/hoare_logic/blocking_semantics3.mlw
+++ b/examples/hoare_logic/blocking_semantics3.mlw
--- a/examples/hoare_logic/blocking_semantics3/blocking_semantics3_HoareLogic_assert_rule_1.v
+++ b/examples/hoare_logic/blocking_semantics3/blocking_semantics3_HoareLogic_assert_rule_1.v
--- a/examples/hoare_logic/blocking_semantics3/blocking_semantics3_HoareLogic_assert_rule_ext_1.v
+++ b/examples/hoare_logic/blocking_semantics3/blocking_semantics3_HoareLogic_assert_rule_ext_1.v