Email Gateway (Aug 18 2022 at 19:13): Email Gateway (Aug 18 2022 at 19:13):From: Lars Noschinski <noschinl@in.tum.de>
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
Check_Connected_Impl.thy
Email Gateway (Aug 18 2022 at 19:13):From: Lars Noschinski <noschinl@in.tum.de>
I finally found the reason for this behaviour: The VCG expects the
specification to have an object level quantifier instead of free variables.
-- Lars
Last updated: Apr 26 2024 at 04:17 UTC