Commit 71df38e6 authored 9 years ago by Nicolas Voirol

Relaxed quantification checks and added testcases

parent dad26d13

Branches

Tags

No related merge requests found

Hide whitespace changes

Inline Side-by-side

Showing

src/main/scala/leon/purescala/Quantification.scala 16 additions, 25 deletions

src/main/scala/leon/purescala/Quantification.scala
src/test/resources/regression/verification/purescala/invalid/BinarySearchTreeQuant.scala 42 additions, 0 deletions

...erification/purescala/invalid/BinarySearchTreeQuant.scala
src/test/resources/regression/verification/purescala/valid/BinarySearchTreeQuant.scala 42 additions, 0 deletions

.../verification/purescala/valid/BinarySearchTreeQuant.scala
testcases/verification/datastructures/BinarySearchTreeQuant.scala 42 additions, 0 deletions

...s/verification/datastructures/BinarySearchTreeQuant.scala
testcases/verification/quantification/invalid/BinarySearchTreeQuant.scala 42 additions, 0 deletions

...cation/quantification/invalid/BinarySearchTreeQuant.scala
testcases/verification/quantification/invalid/HOInvocations.scala 16 additions, 0 deletions

...s/verification/quantification/invalid/HOInvocations.scala
testcases/verification/quantification/invalid/Monotonic.scala 10 additions, 0 deletions

...cases/verification/quantification/invalid/Monotonic.scala
testcases/verification/quantification/invalid/PositiveMap.scala 23 additions, 0 deletions

...ses/verification/quantification/invalid/PositiveMap.scala
testcases/verification/quantification/invalid/Postcondition.scala 14 additions, 0 deletions

...s/verification/quantification/invalid/Postcondition.scala
testcases/verification/quantification/invalid/Simple.scala 20 additions, 0 deletions

testcases/verification/quantification/invalid/Simple.scala
testcases/verification/quantification/invalid/SizeInc.scala 17 additions, 0 deletions

testcases/verification/quantification/invalid/SizeInc.scala
testcases/verification/quantification/valid/BinarySearchTreeQuant.scala 42 additions, 0 deletions

...fication/quantification/valid/BinarySearchTreeQuant.scala
testcases/verification/quantification/valid/Composition.scala 14 additions, 0 deletions

...cases/verification/quantification/valid/Composition.scala
testcases/verification/quantification/valid/HOInvocations.scala 17 additions, 0 deletions

...ses/verification/quantification/valid/HOInvocations.scala
testcases/verification/quantification/valid/Monotonic.scala 10 additions, 0 deletions

testcases/verification/quantification/valid/Monotonic.scala
testcases/verification/quantification/valid/PositiveMap.scala 33 additions, 0 deletions

...cases/verification/quantification/valid/PositiveMap.scala
testcases/verification/quantification/valid/Postcondition.scala 23 additions, 0 deletions

...ses/verification/quantification/valid/Postcondition.scala
testcases/verification/quantification/valid/Relations.scala 31 additions, 0 deletions

testcases/verification/quantification/valid/Relations.scala
testcases/verification/quantification/valid/Simple.scala 44 additions, 0 deletions

testcases/verification/quantification/valid/Simple.scala
testcases/verification/quantification/valid/SizeInc.scala 26 additions, 0 deletions

testcases/verification/quantification/valid/SizeInc.scala

with 524 additions and 25 deletions

Please register or to comment