Re: [isabelle] VCG of Simpl throws exception



On 22.02.2012 10:22, Lars Noschinski wrote:
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

I finally found the reason for this behaviour: The VCG expects the specification to have an object level quantifier instead of free variables.

  -- Lars





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