Korat - Screenshots

Korat Screenshots

These screenshots show Korat's visualization of generated structures. The specific example illustrates how visualization can assist users in correcting repOk (invariant) methods. The example considers a simple binary tree. The first incorrect repOk only checks that every node reachable from itself is not reachable from the root. While this prevents cycles, it does allow sharing (and effectively checks that the input structure is a DAG).

(One of the graphs is not a tree, which means that repOk is incorrect.)

(An attempt that rules out some simple cases of sharing still results in a repOk that is incorrect.)