Last active
October 2, 2022 10:43
-
-
Save jovaneyck/0758d5c352bec696ffe133d77bc61b8c to your computer and use it in GitHub Desktop.
Example properties for a binary search tree implementation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
//Inspired on "How to specify it!" by John Hughes (& Java adaptation by Johannes Link) | |
//https://johanneslink.net/how-to-specify-it/ | |
#r "nuget: fscheck" | |
open FsCheck | |
module BST = | |
type BinarySearchTree<'v> = | |
| Empty | |
| Node of | |
{| left: BinarySearchTree<'v> | |
value: 'v | |
right: BinarySearchTree<'v> |} | |
let empty = Empty | |
let rec add v t = | |
match t with | |
| Empty -> | |
Node | |
{| value = v | |
left = Empty | |
right = Empty |} | |
| Node node when v <= node.value -> | |
Node | |
{| node with | |
left = node.left |> add v |} | |
| Node node -> | |
Node | |
{| node with | |
right = node.right |> add v |} | |
let rec toList t = | |
match t with | |
| Empty -> [] | |
| Node n -> | |
List.concat [ n.left |> toList | |
[ n.value ] | |
n.right |> toList ] | |
let rec ofList l = | |
match l with | |
| [] -> Empty | |
| h :: t -> (ofList t) |> add h | |
let rec contains v t = | |
match t with | |
| Empty -> false | |
| Node n -> | |
n.value = v | |
|| n.left |> contains v | |
|| n.right |> contains v | |
let union t1 t2 = | |
t1 | |
|> toList | |
|> List.fold (fun s x -> s |> add x) t2 | |
//Interesting part about BST: it's possible to represent illegal states | |
//as the sorted invariant is not encoded into its type | |
//That's why we need a custom arbitrary | |
type IntTree = BST.BinarySearchTree<int> | |
type EquivalentTrees = IntTree * IntTree | |
type Arbitraries = | |
static member BST<'v when 'v: comparison>() = | |
Arb.from<'v list> | |
|> Arb.convert BST.ofList BST.toList | |
static member EquivalentTrees() = | |
Arb.from<int list> | |
|> Arb.toGen | |
|> Gen.map (fun xs -> BST.ofList xs, BST.ofList (List.sort xs)) | |
|> Arb.fromGen | |
Arb.register<Arbitraries> () | |
let rec validTree (t: IntTree) = | |
match t with | |
| BST.BinarySearchTree.Empty -> true | |
| BST.BinarySearchTree.Node n when n.left |> validTree && n.right |> validTree -> | |
let ls = n.left |> BST.toList | |
let rs = n.right |> BST.toList | |
ls |> List.forall (fun l -> l <= n.value) | |
&& rs |> List.forall (fun r -> r > n.value) | |
| _ -> false | |
let equivalent t1 t2 = t1 |> BST.toList = (t2 |> BST.toList) | |
//Invariant: any BST is sorted | |
Check.Quick("invariant. If I fail the arbitrary generates invalid trees!", (fun t -> t |> validTree)) | |
//Checking arbitraries: EquivalentTrees are always equivalent | |
Check.Quick("verifying equivalence", (fun ((t1, t2): EquivalentTrees) -> equivalent t1 t2)) | |
//Validity testing | |
Check.Quick("empty-valid", (fun () -> BST.BinarySearchTree.Empty |> validTree)) | |
Check.Quick("add-valid", (fun (t: IntTree) x -> t |> BST.add x |> validTree)) | |
Check.Quick("union-valid", (fun (t1: IntTree) (t2: IntTree) -> BST.union t1 t2 |> validTree)) | |
//Postconditions for add | |
Check.Quick("add-always contains x", (fun (t: IntTree) x -> t |> BST.add x |> BST.contains x)) | |
Check.Quick( | |
"add-always grows tree by 1", | |
(fun (t: IntTree) x -> | |
let l = t |> BST.toList |> List.length | |
let added = t |> BST.add x | |
let al = added |> BST.toList |> List.length | |
al = l + 1) | |
) | |
Check.Quick( | |
"add-always contains original values", | |
fun (t: IntTree) x -> | |
let origs = t |> BST.toList | |
let added = t |> BST.add x | |
origs | |
|> List.forall (fun o -> added |> BST.contains o) | |
) | |
//Metamorphic properties: related calls return related results | |
Check.Quick("add-add", (fun (t: IntTree) a b -> equivalent (BST.add a (BST.add b t)) (BST.add b (BST.add a t)))) | |
Check.Quick( | |
"add-union", | |
(fun (t1: IntTree) (t2: IntTree) x -> equivalent (BST.add x (BST.union t1 t2)) (BST.union (BST.add x t1) t2)) | |
) | |
Check.Quick("union-commutative", (fun (t1: IntTree) (t2: IntTree) -> equivalent (BST.union t1 t2) (BST.union t2 t1))) | |
//Equivalence | |
Check.Quick( | |
"add-preserves equivalence", | |
fun ((t1, t2): EquivalentTrees) x -> equivalent (BST.add x t1) (BST.add x t2) | |
) | |
Check.Quick( | |
"union-preserves equivalence", | |
fun (t: IntTree) ((t1, t2): EquivalentTrees) -> equivalent (BST.union t1 t) (BST.union t2 t) | |
) | |
//Induction | |
Check.Quick("union-zero", (fun (t1: IntTree) -> equivalent t1 (BST.union t1 BST.BinarySearchTree.Empty))) | |
Check.Quick( | |
"any list can be created by its insertions", | |
(fun (t: IntTree) -> equivalent t (t |> BST.toList |> BST.ofList)) | |
) | |
//Model-based | |
Check.Quick( | |
"add-model", | |
(fun (t: IntTree) x -> | |
let xs = t |> BST.toList | |
let addedList = (x :: xs) |> List.sort | |
let addedTree = t |> BST.add x | |
(addedTree |> BST.toList) = addedList) | |
) | |
Check.Quick( | |
"union-model", | |
(fun (t1: IntTree) (t2: IntTree) -> | |
let listUnion = | |
(t1 |> BST.toList) @ (t2 |> BST.toList) | |
|> List.sort | |
let treeUnion = BST.union t1 t2 | |
(treeUnion |> BST.toList) = listUnion) | |
) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment