search

braibant / articheck

14 stars 2 forks source link

Example list #3

Closed braibant closed 10 years ago

braibant commented 10 years ago

Find an example with at least two different abstract types (e.g., a programming language with two different syntactic categories) to check non trivial properties

braibant commented 10 years ago

Other examples include data-types with non-trivial invariant, e.g., being an binary search tree for AVLs, or persistent data-structures, or hash-consed data-structures. Here be BDDs.

gasche commented 10 years ago

I'm adding zippers to RBT, on a suggestion by François. This should give us an example with both interesting invariants and two distinct abstract types.