-
Notifications
You must be signed in to change notification settings - Fork 38
Add support for property-based testing #893
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Open
lenakaeufel
wants to merge
41
commits into
effekt-lang:master
Choose a base branch
from
lenakaeufel:lenakaeufel/thesis-pbt
base: master
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Open
Changes from 1 commit
Commits
Show all changes
41 commits
Select commit
Hold shift + click to select a range
4288b42
thesis-pbt-effekt: add property-based testing support to stdlib testi…
28e8d45
Fix: Splices with non-String type break if there is no splice (#901)
dvdvgt e1b92bb
Add lambda calculus NbE example/benchmark (#898)
marvinborner fe047ce
Run tests without optimization (#851)
marvinborner 6f8b155
Fix inferring effectful while header (#902)
PhictionalOne 9195bbe
Allow trailing comma in list literals (#900)
mattisboeckle 7219512
Standalone language server (#885)
timsueberkrueb d2bdb9f
Fix: make type pretty printer less confusing for boxed types (#906)
dvdvgt 3773ff2
Add test for cyclic imports (#903)
marzipankaiser ee78f84
Bump to llvm version 18 in CI (#887)
mattisboeckle 67f47cb
Improve performance of state (#907)
b-studios 9ba3cfa
Fix lsp caching issues (#894)
timsueberkrueb 86ebd77
Fix: ufcs integer lexing (#912)
dvdvgt 1a71751
Add binary search benchmark (#904)
jiribenes 9b9266c
Properly represent existentials in core (#880)
phischu 87a080d
Allow lambda case patterns for multiple parameters (#914)
marzipankaiser 4b8434e
Fix failing tests without optimization (#890)
marvinborner 739914c
Go via trampoline in machine transformer (#917)
phischu 8460593
Fix: dot notation using block params (#918)
dvdvgt 895cafb
Bump version to 0.25.0
effekt-updater[bot] 387b3e7
CI: Fix npm provenance
jiribenes 2a9a36c
CI: Add a way to publish manually to npm
jiribenes 717940a
Fix invalid links (#927)
dvdvgt a8d3b93
Reimplement C utilities in llvm (#910)
mattisboeckle e417c07
JSWeb: report all collected errors upon aborting (#931)
dvdvgt 6d9b29b
Bump version to 0.26.0
effekt-updater[bot] f669047
Remove debug print in Normalizer (#937)
jiribenes 70fb283
Simplify core.Renamer to produce smaller symbols (#938)
jiribenes d6472ec
Don't reallocate StringBuffer when flushing (#939)
jiribenes 73edfdc
Renamer: Add infrastructure for Checking Uniqueness of Generated Name…
marzipankaiser 28edaf2
Make 'core.Renamer' quicker by simplifying scope handling (#940)
jiribenes 62b505f
Add tailrec annotations wherever possible (#945)
jiribenes d305794
Bump version to 0.27.0
effekt-updater[bot] 1ba0939
Cache substitutions (#954)
b-studios 28200a2
Specific info message for equally named effect operations (#956)
JakubSchwenkbeck 16f0ce8
Bump version to 0.28.0
effekt-updater[bot] 990fe10
Add wellformedness check for type of `var ... in ...` (#961)
marzipankaiser 298d186
LLVM: Emit most declared definitions as private (#946)
mattisboeckle d42294b
Add bytestream-based 'random' module with PRNG and /dev/urandom handl…
jiribenes 2f58c0d
use the random effect instead of FFI
539a8ae
added check files for golden tests, removed leftover debug print
File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or 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
Original file line number | Diff line number | Diff line change | ||
---|---|---|---|---|
@@ -0,0 +1,166 @@ | ||||
import test | ||||
|
||||
def main() = { | ||||
println(suite("PBT: List Functions and Other Simple Examples") { | ||||
|
||||
// example unit tests to show that mixed test suites work | ||||
test("1 + 1 == 2") { | ||||
assertEqual(1 + 1, 2) | ||||
} | ||||
|
||||
test("2 + 2 == 3") { | ||||
assertEqual(2 + 2, 3) | ||||
} | ||||
|
||||
// reverse[x] === [x] | ||||
with arbitraryInt; | ||||
forall[Int]("reverse-singleton", 100){ x => | ||||
assertEqual( | ||||
reverse([x]), | ||||
[x] | ||||
) | ||||
} | ||||
Comment on lines
+20
to
+27
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. When you add the checkfiles, this will probably fail for two reasons on LLVM:
where you might need to define equality on lists in |
||||
|
||||
// reverse[x] === [x], with explicit passing of the generator | ||||
with def g = arbitraryInt; | ||||
forall[Int]("reverse-singleton, explicitely passing the generator", 100){ g } | ||||
{ x => | ||||
assertEqual( | ||||
reverse([x]), | ||||
[x] | ||||
) | ||||
} | ||||
|
||||
// intented mistake: reverse[x] === [6] | ||||
forall[Int]("reverse-singleton mistake", 100) | ||||
{ x => | ||||
assertEqual( | ||||
reverse([x]), | ||||
[6] | ||||
) | ||||
} | ||||
|
||||
// shows that exists prints tried test cases and found examples correctly | ||||
exists[Int]("Is the Integer 2 among the generated values?", 100) | ||||
{ x => | ||||
assertEqual( | ||||
x, | ||||
2 | ||||
) | ||||
} | ||||
|
||||
// reverse(xs ++ ys) === reverse(ys) ++ reverse(xs) | ||||
with arbitraryList[Int](3) | ||||
forall[List[Int], List[Int]]("reverse: distributivity over append", 100) | ||||
{ (xs, ys) => | ||||
assertEqual( | ||||
reverse(xs.append(ys)), | ||||
reverse(ys).append(reverse(xs)) | ||||
) | ||||
} | ||||
|
||||
// intended mistake: reverse(xs ++ ys) === reverse(xs) ++ reverse(ys) | ||||
forall[List[Int], List[Int]]("reverse: distributivity mistake - swapped order", 20) | ||||
{ (xs, ys) => | ||||
assertEqual( | ||||
reverse(xs.append(ys)), | ||||
reverse(xs).append(reverse(ys)) | ||||
) | ||||
} | ||||
|
||||
with arbitraryChar; | ||||
with arbitraryList[Char](4); | ||||
forall[List[Char], List[Int]]("|zip(xs,ys)| === min(|xs|,|ys|)",10) | ||||
{ (xs, ys) => | ||||
assertEqual( | ||||
zip(xs, ys).size, | ||||
min(xs.size, ys.size) | ||||
) | ||||
} | ||||
|
||||
with arbitraryChar; | ||||
with arbitraryList[Char](6); | ||||
forall[List[Char], List[Int]]("intended mistake: |zip(xs,ys)| != max(|xs|,|ys|)",10) | ||||
{ (xs, ys) => | ||||
assertEqual( | ||||
zip(xs, ys).size, | ||||
max(xs.size, ys.size) | ||||
) | ||||
} | ||||
|
||||
// unzip(zip(xs,ys)) === (xs.take(m), ys.take(m)) where m = min(|xs|,|ys|) | ||||
with arbitraryChar; | ||||
with arbitraryString(4); | ||||
with arbitraryList[String](2); | ||||
with arbitraryInt; | ||||
with arbitraryList[Int](3) | ||||
forall[List[Int], List[String]]("unzip-zip-take relation", 10) | ||||
{ (xs, ys) => | ||||
val m = min(xs.size, ys.size) | ||||
assertEqual( | ||||
unzip(zip(xs, ys)), | ||||
(xs.take(m), ys.take(m)) | ||||
) | ||||
} | ||||
|
||||
// Dropping elements from the concatenation of two lists is equivalent to dropping elements from the first list, | ||||
// and then (if necessary) dropping the remaining count from the second list. | ||||
// (xs ++ ys).drop(n) === if n <= len(xs) then (xs.drop(n)) ++ ys else ys.drop(n - len(xs)) | ||||
forall[List[Int], List[Int], Int]("drop: concatenation ", 10) | ||||
{ (xs, ys, n) => | ||||
val res = if(n <= xs.size) { | ||||
xs.drop(n).append(ys) | ||||
} | ||||
else { ys.drop(n - xs.size) } | ||||
assertEqual( | ||||
(xs.append(ys).drop(n)), | ||||
res | ||||
) | ||||
} | ||||
|
||||
// xs.drop(n) === xs.slice(n, x.size) | ||||
forall[List[Int], Int]("drop-slice relation", 10) | ||||
{ (xs, n) => | ||||
assertEqual( | ||||
xs.drop(n), | ||||
xs.slice(n, xs.size) | ||||
) | ||||
} | ||||
|
||||
// reverseOnto(reverse(xs), ys) === append(xs, ys) | ||||
forall[List[Int], List[Int]]("reverseOnto-reverse-append relation ", 10) | ||||
{ (xs, ys) => | ||||
assertEqual( | ||||
reverseOnto(reverse(xs), ys), | ||||
append(xs, ys) | ||||
) | ||||
} | ||||
|
||||
// size(xs) === foldLeft(xs, 0) { (acc, _) => acc + 1 } | ||||
forall[List[Int]]("size-foldLeft relation", 20) | ||||
{ xs => | ||||
assertEqual( | ||||
size(xs), | ||||
foldLeft(xs, 0){(acc, _) => acc + 1} | ||||
) | ||||
} | ||||
|
||||
//xs.take(n) ++ xs.drop(n) === xs | ||||
forall[Int, List[Int]]("take-drop: inversion over concatenation", 20) | ||||
{ (n, xs) => | ||||
assertEqual( | ||||
append(xs.take(n), xs.drop(n)), | ||||
xs | ||||
) | ||||
} | ||||
|
||||
// example for a property-based test with multiple assertions | ||||
with evenNumbers; | ||||
forall[Int]("even numbers are even and smaller than 4", 20) | ||||
{ n => | ||||
assertTrue(n.mod(2) == 0) | ||||
assertTrue(n <= 4) | ||||
} | ||||
}) | ||||
} | ||||
|
This file contains hidden or 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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,107 @@ | ||
import map | ||
import stream | ||
|
||
import test | ||
|
||
// user-defined generator for arbitrary, unique Integers in ascending order | ||
def uniqueInt{body: => Unit / Generator[Int]}: Unit = { | ||
try body() with Generator[Int]{ | ||
def generate() = resume{ | ||
var next = randomInt(-100, 100) | ||
do emit(next) | ||
while(true){ | ||
next = next + randomInt(1, 5) | ||
do emit(next) | ||
} | ||
} | ||
def shrink(v) = <> | ||
} | ||
} | ||
|
||
// precondition: provided handler for Generator[K] needs to produce unique keys in ascending order! | ||
// otherwise the generated trees aren't valid binary search trees | ||
def arbitraryBinTree[K, V] (numKeys: Int) { body: => Unit / Generator[internal::Tree[K, V]] }: Unit / {Generator[K], Generator[V]} = { | ||
def buildTree[K, V](pairs: List[(K, V)]): internal::Tree[K,V] = { | ||
if (pairs.isEmpty) { | ||
internal::Tip() | ||
} else { | ||
val midIdx = pairs.size() / 2 | ||
with on[OutOfBounds].panic; | ||
val midEl = pairs.get(midIdx) | ||
val leftTree = buildTree(pairs.take(midIdx)) | ||
val rightTree = buildTree(pairs.drop(midIdx + 1)) | ||
val size = 1 + internal::size(leftTree) + internal::size(rightTree) | ||
|
||
internal::Bin(size, midEl.first, midEl.second, leftTree, rightTree) | ||
} | ||
} | ||
|
||
try body() with Generator[internal::Tree[K, V]] { | ||
def generate() = resume { | ||
while(true) { | ||
val l1 = collectList[K]{with boundary; with limit[K](numKeys); do generate[K]} | ||
val l2 = collectList[V]{with boundary; with limit[V](numKeys); do generate[V]} | ||
val sortedPairs = zip(l1,l2) | ||
do emit(buildTree[K, V](sortedPairs)) | ||
//TODO try to use zip again | ||
} | ||
} | ||
def shrink(v) = <> | ||
} | ||
} | ||
|
||
def main()= { | ||
with arbitraryChar; | ||
with arbitraryString(5); | ||
with uniqueInt; | ||
with arbitraryBinTree[Int, String](8); | ||
|
||
println(suite("PBT: Tree Map Examples") { | ||
lenakaeufel marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
|
||
|
||
// get-put law: get(put(M, K, V), K) = V | ||
forall[String, internal::Tree[Int, String], Int]("get-put law", 100) | ||
{ (v, t, k) => | ||
val newT = internal::put(t, compareInt, k, v) | ||
internal::get(newT, compareInt, k) match { | ||
case Some(value) => assertEqual(value, v) | ||
case None() => do assert(false, "Key not in the tree") | ||
} | ||
} | ||
|
||
// put-put law: get(put(put(M, K, V1), K, V2), K) = V2 | ||
forall[String, internal::Tree[Int, String], Int]("put-put law", 100) | ||
{ (v1, t, k) => | ||
val v2 = v1 ++ show(k) ++ v1 | ||
val newT1 = internal::put(t, compareInt, k, v1) | ||
val newT2 = internal::put(newT1, compareInt, k, v2) | ||
internal::get(newT2, compareInt, k) match { | ||
case Some(v) => assertEqual(v, v2) | ||
case None() => do assert(false, "Key in the tree") | ||
} | ||
} | ||
|
||
// put-get law: put(M, K, get(M, K)) = M | ||
forall[internal::Tree[Int, String]]("put-get law", 100) | ||
{ t => | ||
// put-get law only make sense if K is present in the tree ~> get the keys of the tree | ||
var keys = Nil() | ||
t.internal::foreach[Int, String] { (k, _v) => keys = Cons(k, keys)} | ||
|
||
with on[OutOfBounds].panic | ||
val k = keys.get(randomInt(0, keys.size())) // only check the property for key's present in the tree (= non trivial test case) | ||
internal::get(t, compareInt, k) match { | ||
case Some(v) => { | ||
val newT = internal::put(t, compareInt, k, v) | ||
assertEqual(t, newT)} | ||
case None() => do assert(false, "Key not in the tree") | ||
} | ||
} | ||
|
||
// Law: `m.forget === m.map { (_k, _v) => () } | ||
forall[internal::Tree[Int, String]]("forget-map relation", 100){t => | ||
val tForget = internal::forget(t) | ||
val tMap = internal::map(t){ (_k, _v) => ()} | ||
assertEqual(tForget, tMap) | ||
} | ||
}) | ||
} |
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.