equal
deleted
inserted
replaced
7 |
7 |
8 Quick Usage |
8 Quick Usage |
9 |
9 |
10 - Import Spec_Check.thy in your development |
10 - Import Spec_Check.thy in your development |
11 - Look at examples in Examples.thy |
11 - Look at examples in Examples.thy |
12 - write specifications with the ML function |
12 - write specifications with the ML invocation |
13 Spec_Check.check_property @{context} "ALL x. P x" |
13 check_property "ALL x. P x" |
14 |
14 |
15 Notes |
15 Notes |
16 |
16 |
17 Our specification-based testing tool originated from Christopher League's |
17 Our specification-based testing tool originated from Christopher League's |
18 QCheck tool for SML (cf. https://github.com/league/qcheck). As Isabelle |
18 QCheck tool for SML (cf. https://github.com/league/qcheck). As Isabelle |