Theory SpecCheck_Examples

✐‹creator "Kevin Kappelmann"›
section ‹Examples›
theory SpecCheck_Examples
imports SpecCheck_Dynamic
begin

ML ‹
open SpecCheck
open SpecCheck_Dynamic
structure Gen = SpecCheck_Generator
structure Prop = SpecCheck_Property
structure Show = SpecCheck_Show
structure Shrink = SpecCheck_Shrink
structure Random = SpecCheck_Random
›

subsection ‹Unit Tests and Exceptions›

ML ‹
  fun faulty_abs n =
    if n < ~10000 then error "out of bounds"
    else if n < 0 then ~n
    else n
›

ML_command ‹
let
  val check_unit_int_pair = check_unit_tests (Show.zip Show.int Show.int)
  fun correctness_tests ctxt s = Lecker.test_group ctxt s [
      check_unit_int_pair  [(~10, 10), (0, 0), (10, 10)] "correctness small values"
        (Prop.prop (fn (n, exp) => faulty_abs n = exp)),
      check_unit_int_pair [(~999999999, 999999999), (999999999, 999999999)]
        "correctness large values" (Prop.prop (fn (n, exp) => faulty_abs n = exp))
    ]
  fun exception_tests ctxt s =
    let val exn_prop = Prop.expect_failure (ERROR "out of bounds") faulty_abs
    in
      Lecker.test_group ctxt s [
        check_unit_tests Show.int [~10, 0, 10] "expect exception for small values" exn_prop,
        check_unit_tests Show.int [~999999999, ~99999999999999] "expect exception for large values"
          exn_prop
      ]
    end
in
  Lecker.test_group @{context} () [
    check_unit_tests Show.int [~10, 0, 10] "is idempotent"
      (Prop.prop (fn n => faulty_abs (faulty_abs n) = faulty_abs n)),
    correctness_tests,
    exception_tests
  ]
end
›

subsection ‹Randomised Tests›

ML_command ‹
let
  val int_gen = Gen.range_int (~10000000, 10000000)
  val size_gen = Gen.nonneg 10
  val check_list = check_shrink (Show.list Show.int) (Shrink.list Shrink.int)
    (Gen.list size_gen int_gen)
  fun list_test (k, f, xs) =
    AList.lookup (op=) (AList.map_entry (op=) k f xs) k = Option.map f (AList.lookup (op=) xs k)

  val list_test_show = Show.zip3 Show.int Show.none (Show.list (Show.zip Show.int Show.int))
  val list_test_gen = Gen.zip3 int_gen (Gen.function' int_gen)
    (Gen.list size_gen (Gen.zip int_gen int_gen))
in
  Lecker.test_group @{context} (Random.new ()) [
    Prop.prop (fn xs => rev xs = xs) |> check_list "rev = I",
    Prop.prop (fn xs => rev (rev xs) = xs) |> check_list "rev o rev = I",
    Prop.prop list_test |> check list_test_show list_test_gen "lookup map equiv map lookup"
  ]
end
›

text ‹The next three examples roughly correspond to the above test group (except that there's no
shrinking). Compared to the string-based method, the method above is more flexible - you can change
your generators, shrinking methods, and show instances - and robust - you are not reflecting strings
(which might contain typos) but entering type-checked code. In exchange, it is a bit more work to
set up the generators. However, in practice, one shouldn't rely on default generators in most cases
anyway.›

ML_command ‹
check_dynamic @{context} "ALL xs. rev xs = xs";
›

ML_command ‹
check_dynamic @{context} "ALL xs. rev (rev xs) = xs";
›

subsection ‹AList Specification›

ML_command ‹
(*map_entry applies the function to the element*)
check_dynamic @{context} (implode
  ["ALL k f xs. AList.lookup (op =) (AList.map_entry (op =) k f xs) k = ",
   "Option.map f (AList.lookup (op =) xs k)"])
›

ML_command ‹
(*update always results in an entry*)
check_dynamic @{context} "ALL k v xs. AList.defined (op =) (AList.update (op =) (k, v) xs) k";
›

ML_command ‹
(*update always writes the value*)
check_dynamic @{context}
  "ALL k v xs. AList.lookup (op =) (AList.update (op =) (k, v) xs) k = SOME v";
›

ML_command ‹
(*default always results in an entry*)
check_dynamic @{context} "ALL k v xs. AList.defined (op =) (AList.default (op =) (k, v) xs) k";
›

ML_command ‹
(*delete always removes the entry*)
check_dynamic @{context} "ALL k xs. not (AList.defined (op =) (AList.delete (op =) k xs) k)";
›

ML_command ‹
(*default writes the entry iff it didn't exist*)
check_dynamic @{context} (implode
  ["ALL k v xs. (AList.lookup (op =) (AList.default (op =) (k, v) xs) k = ",
   "(if AList.defined (op =) xs k then AList.lookup (op =) xs k else SOME v))"])
›

subsection ‹Examples on Types and Terms›

ML_command ‹
check_dynamic @{context} "ALL f g t. map_types (g o f) t = (map_types f o map_types g) t";
›

ML_command ‹
check_dynamic @{context} "ALL f g t. map_types (f o g) t = (map_types f o map_types g) t";
›


text ‹One would think this holds:›

ML_command ‹
check_dynamic @{context} "ALL t ts. strip_comb (list_comb (t, ts)) = (t, ts)"
›

text ‹But it only holds with this precondition:›

ML_command ‹
check_dynamic @{context}
  "ALL t ts. case t of _ $ _ => true | _ => strip_comb (list_comb (t, ts)) = (t, ts)"
›

subsection ‹Some surprises›

ML_command ‹
check_dynamic @{context} "ALL Ts t. type_of1 (Ts, t) = fastype_of1 (Ts, t)"
›


ML_command ‹
val thy = \<^theory>;
check_dynamic (Context.the_local_context ())
  "ALL t u. if Pattern.matches thy (t, u) then Term.could_unify (t, u) else true"
›

end