Re: [isabelle] Disproof methods with Word.thy and AutoCorres



Hi Andreas,

Thanks for your suggestions about writing some custom state generators.
I have some ideas about what might be useful testcases in practice.

Generating custom states by inspecting the precondition sounds fun, but
might be a longer-term project. :)

On 05/11/14 20:34, Andreas Lochbihler wrote:
[...]
> I was not able to look at problem 2, because I have not found a small
> example where the ptr causes an exception. If you provide one, I can
> have a look at this, too.

I have attached a small, self-contained example that demonstrates the
problem.

In particular:

    lemma "(a :: nat ptr ⇒ nat) = b"
      quickcheck

seems to work fine, but:

    record lifted_globals =
      foo :: "nat ptr ⇒ nat"

    lemma "(a :: lifted_globals) = b"
      quickcheck

raises one of the errors:

    Wellsortedness error
    (in code equation equal_lifted_globals_ext_inst.equal_lifted_globals_ext
                       ⦇foo = ?fooa, … = ?morea⦈ ⦇foo = ?foo, … = ?more⦈ ≡
                      ?fooa = ?foo ∧ ?morea = ?more,
    with dependency "Pure.dummy_pattern" -> "equal_class.equal [lifted_globals_ext]"):
    Type nat ptr ⇒ nat not of sort equal
    No type arity ptr :: enum

or:

    Error: Type 'a ptr list includes a free type variable
    val
       enum_ptra : 'a ptr list =
          map (Ptr o ... ...) (upt Zero_nat (... ... (... ...)))
    At (line 1331 of "generated code")
    Error: Type mismatch in type constraint.
       Value:
          {finite_enum = finite_ptr, enum = enum_ptra, enum_all = enum_all_ptr,
            enum_ex = enum_ex_ptr} :
          {enum: 'a ptr list,
            enum_all: ('b -> bool) -> bool,
            enum_ex: ('c -> bool) -> bool, finite_enum: 'd ptr finite}
       Constraint: 'a ptr enum
       Reason: Can't unify 'a to 'a (Cannot unify with explicit type variable)
    {finite_enum = finite_ptr, enum = enum_ptra, enum_all = enum_all_ptr,
         enum_ex = ...} : 'a ptr enum
    At (line 1351 of "generated code")
    Exception- Fail "Static Errors" raised

Depending on whether "ptr" has been instantiated into the "enum" class
or not, respectively.

Thanks for your help,
David


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
theory PtrTypeQuickcheck
imports "~~/src/HOL/Word/Word"
begin

datatype 'a ptr = Ptr "32 word"

(* Setup "word" and "ptr" types to work with quickcheck. *)

quickcheck_generator word
  constructors:
    "zero_class.zero :: ('a::len) word",
    "numeral :: num \<Rightarrow> ('a::len) word",
    "uminus :: ('a::len) word \<Rightarrow> ('a::len) word"

quickcheck_generator ptr constructors: Ptr

(* This works fine... *)
lemma "(a :: nat ptr \<Rightarrow> nat) = b"
  quickcheck
  oops

(* ...but when we move it into a record... *)
record lifted_globals =
  foo :: "nat ptr \<Rightarrow> nat"

(* This produces an error complaining about the lack of the "enum" class of ptr. *)
lemma "(a :: lifted_globals) = b"
  quickcheck
  oops

(* We can try instantiating "ptr" into the enum class... *)
instantiation ptr :: (type) enum
begin
  definition "enum_ptr \<equiv> map (Ptr o of_nat) [0 ..< 2 ^ 32]"
  definition "enum_all_ptr (P :: 'a ptr \<Rightarrow> bool) \<equiv> Ball UNIV P"
  definition "enum_ex_ptr (P :: 'a ptr \<Rightarrow> bool) \<equiv> Bex UNIV P"
  instance sorry
end

(* ...but not we get the error: "Type 'a ptr list includes a free type variable" *)
lemma "(a :: lifted_globals) = b"
  quickcheck
  oops

end


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