CozySynthesizer / cozy

The collection synthesizer
https://cozy.uwplse.org
Apache License 2.0
209 stars 18 forks source link

Some sample specs not accepted by cozy #3

Closed seizethedave closed 7 years ago

seizethedave commented 7 years ago

Fix them.

agg.ds

disjunction.ds

$ cozy --simple disjunction.ds --java -

In:
  type Elem = Elem
  state xs : Set<Elem>
  query a(st : Int, ed : Int):
    [x | x <- xs, ((((x).val).0 == st) or (((x).val).1 == ed))]
  op add(e : Elem):
    xs.add(e)

In:
  type Elem = Elem
  state xs : Bag<Elem>
  assume (unique xs);
  query a(st : Int, ed : Int):
    Filter {(\x -> ((((x).val).0 == st) or (((x).val).1 == ed)))} (xs)
  op add(e : Elem):
    xs.add(e)

Error: 'add' may not preserve invariant (unique xs)

graph.ds

$ cozy --simple graph.ds --java -
...
Error: 'addEdge' may not preserve invariant ((sum Map {(\e -> 1)} (Filter {(\e -> (((e).val).src == ((e).val).dst))} (edges))) == 0)

intset.ds

$ cozy --simple intset.ds --java -
...
Error: 'add' may not preserve invariant (unique ints)