[isabelle] VCG of Simpl throws exception



Hi,

I'm trying to verify some simple program using the Simpl theory from the AFP (2011-1 [1]), but I stumbled on some (probably technical) problem:

I have a procedure for which I proved the following specification:

  lemma (in has_unique_edges_impl) has_unique_edges_spec:
    "Γ ⊢ ⦃ ´G = G ⦄
         ´R :== PROC has_unique_edges(´G)
         ⦃ ´R = has_unique_edges_inv1 G (iedge_cnt G) ⦄"

Now, I try to prove some properties about a call to this procedure:

  lemma (in has_unique_edges_impl)
    "Γ ⊢ ⦃ ´G = G ⦄ ´R :== CALL has_unique_edges(´G)
         ⦃ ´R = has_unique_edges_inv1 G (iedge_cnt G) ⦄"
    apply vcg

This fails with:

exception TERM raised (line 3260 of "/home/noschinl/P/afp/thys/Simpl/hoare.ML"):
FunSplitState.fold_state_prop
x

Instead I tried single-stepping, which generates a number of flex-flex pairs:

    apply vcg_step

goal (1 subgoal):
 1. ⦃´G = G⦄
    ⊆ ⦃´G = ?G21 () ∧
       (∀t. ⇗t⇖R = has_unique_edges_inv1 (?G19 ()) (iedge_cnt (?G18 ())) ⟶
            ⇗t⇖R = has_unique_edges_inv1 G (iedge_cnt G))⦄
flex-flex pairs:
  ?G21 () =?= ?G20 ()
  ?G20 () =?= ?G9 ()
  ?G19 () =?= ?G17 ()
  ?G18 () =?= ?G16 ()
  ?G17 () =?= ?G8 ()
  ?G16 () =?= ?G7 ()
  ?G9 () =?= ?G7 ()
  ?G8 () =?= ?G7 ()

And the next vcg_step produces the error above. So, is this an error in the VCG or has my spec some unexpected format?

  -- Lars

[1] Occurs also with Isabelle 42298c5d33b1 and AFP db765d7a8922
theory Check_Connected_Impl
imports
  "~/P/afp/thys/Simpl/Vcg"
begin

text {* Implemenation *}

type_synonym IVertex = nat
type_synonym IEdge_Id = nat
type_synonym IEdge = "IVertex \<times> IVertex"
type_synonym IGraph = "nat \<times> nat \<times> (IEdge_Id \<Rightarrow> IEdge)" (* last vertex vs. set/list of vertices? *)

abbreviation iedge_cnt :: "IGraph \<Rightarrow> nat"
  where "iedge_cnt G \<equiv> fst (snd G)"

abbreviation iedges :: "IGraph \<Rightarrow> IEdge_Id \<Rightarrow> IEdge"
  where "iedges G \<equiv> snd (snd G)"

definition has_unique_edges_inv1 :: "IGraph \<Rightarrow> nat \<Rightarrow> bool" where
  "has_unique_edges_inv1 G k \<equiv> \<forall>i < k. \<forall>j < iedge_cnt G. i \<noteq> j \<longrightarrow> iedges G i \<noteq> iedges G j"

definition has_unique_edges_inv2 :: "IGraph \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
  "has_unique_edges_inv2 G i k \<equiv> \<forall>j < k. i \<noteq> j \<longrightarrow> iedges G i \<noteq> iedges G j"

procedures has_unique_edges (G :: IGraph | R :: bool)
  where
    i :: nat
    j :: nat
    e1 :: IEdge
    e2 :: IEdge
  in "
    ANNO G.
      \<lbrace> \<acute>G = G \<rbrace>
      \<acute>R :== True ;;
      \<acute>i :== 0 ;;
      TRY
        WHILE \<acute>i < iedge_cnt \<acute>G
        INV \<lbrace> has_unique_edges_inv1 \<acute>G \<acute>i  \<and> \<acute>i \<le> iedge_cnt \<acute>G \<and> \<acute>R = True \<and> \<acute>G = G\<rbrace>
        DO
          \<acute>e1 :== iedges \<acute>G \<acute>i ;;
          \<acute>j :== 0 ;;
          WHILE \<acute>j < iedge_cnt \<acute>G
          INV \<lbrace> has_unique_edges_inv2 \<acute>G \<acute>i \<acute>j \<and> \<acute>e1 = iedges \<acute>G \<acute>i \<and> \<acute>i < iedge_cnt \<acute>G \<and> \<acute>j \<le> iedge_cnt \<acute>G
            \<and> has_unique_edges_inv1 \<acute>G \<acute>i \<and> \<acute>R = True \<and> \<acute>G = G\<rbrace>
          DO
            \<acute>e2 :== iedges \<acute>G \<acute>j ;;
            IF \<acute>i \<noteq> \<acute>j \<and> fst \<acute>e1 = fst \<acute>e2 \<and> snd \<acute>e1 = snd \<acute>e2 THEN
              \<acute>R :== False ;;
              THROW
            FI ;;
            \<acute>j :== \<acute>j + 1
          OD ;;
          \<acute>i :== \<acute>i + 1
        OD
      CATCH SKIP END
      \<lbrace> \<acute>G = G \<and> \<acute>R = has_unique_edges_inv1 \<acute>G (iedge_cnt \<acute>G) \<rbrace>
   "

procedures is_proper_graph (G :: IGraph | R :: bool)
  "\<acute>R :== CALL has_unique_edges(\<acute>G)"

lemma has_unique_edges_inv1_step:
  "has_unique_edges_inv1 G (Suc i) \<longleftrightarrow> has_unique_edges_inv1 G i
    \<and> (\<forall>j < iedge_cnt G. i \<noteq> j \<longrightarrow> iedges G i \<noteq> iedges G j)"
by (auto simp: has_unique_edges_inv1_def less_Suc_eq)

lemma has_unique_edges_inv2_step:
  "has_unique_edges_inv2 G i (Suc j) \<longleftrightarrow> has_unique_edges_inv2 G i j
    \<and> (i \<noteq> j \<longrightarrow> iedges G i \<noteq> iedges G j)"
by (auto simp: has_unique_edges_inv2_def less_Suc_eq)

lemma (in has_unique_edges_impl) has_unique_edges_spec:
  "\<Gamma> \<turnstile> \<lbrace> \<acute>G = G \<rbrace> \<acute>R :== PROC has_unique_edges(\<acute>G) \<lbrace> \<acute>R = has_unique_edges_inv1 G (iedge_cnt G) \<rbrace>"
  apply vcg
  apply (simp_all add: has_unique_edges_inv1_step has_unique_edges_inv2_step)
  apply (auto simp add: has_unique_edges_inv1_def has_unique_edges_inv2_def prod_eq_iff)
  done

lemma (in has_unique_edges_impl)
  "\<Gamma> \<turnstile> \<lbrace> \<acute>G = G \<rbrace> \<acute>R :== CALL has_unique_edges(\<acute>G)
       \<lbrace> \<acute>R \<longleftrightarrow> has_unique_edges_inv1 G (iedge_cnt G) \<rbrace>"
  apply vcg_step
  apply vcg_step
  oops

end


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.