Verifying and Compiling Examples¶
Verifying Examples¶
Stainless is currently available as either:
a command line tool, which exposes most of the functionality, available as a ZIP file (recommended) or via Docker.
via an SBT plugin.
See the installation documentation for more information.
It is henceforth assumed that there exists a stainless script in in your PATH.
To see the main options, use
$ stainless --help
in your command line shell. You may also wish to consult the available command-line options.
You can try some of the examples from frontends/benchmarks
distributed with Stainless:
$ stainless --solvers=smt-cvc5 frontends/benchmarks/verification/invalid/InsertionSort.scala
and get something like this (some output cropped)
[ Info ] Starting verification...
[ Info ] Verified: 3 / 19
[Warning ] - Result for 'postcondition' VC for buggySortedIns @37:38:
[Warning ] l.isInstanceOf[Nil] || !(l.head <= e) || {
[Warning ] val res: List = Cons(l.head, buggySortedIns(e, l.tail))
[Warning ] assume({
[Warning ] val e: List = Cons(l.head, buggySortedIns(e, l.tail))
[Warning ] true
[Warning ] })
[Warning ] contents(res) == contents(l) ++ Set(e) && isSorted(res) && size(res) == size(l) + BigInt("1")
[Warning ] }
[Warning ] frontends/benchmarks/verification/invalid/InsertionSort.scala:37:38: => INVALID
case Cons(x,xs) => if (x <= e) Cons(x,buggySortedIns(e, xs)) else Cons(e, l)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[Warning ] Found counter-example:
[Warning ] l: List -> Cons(-770374653, Cons(-771685886, Nil()))
[Warning ] e: Int -> 1376322050
[ Info ] Verified: 3 / 19
[Warning ] - Result for 'postcondition' VC for buggySortedIns @37:73:
[Warning ] l.isInstanceOf[Nil] || l.head <= e || {
[Warning ] val res: List = Cons(e, l)
[Warning ] contents(res) == contents(l) ++ Set(e) && isSorted(res) && size(res) == size(l) + BigInt("1")
[Warning ] }
[Warning ] frontends/benchmarks/verification/invalid/InsertionSort.scala:37:73: => INVALID
case Cons(x,xs) => if (x <= e) Cons(x,buggySortedIns(e, xs)) else Cons(e, l)
^^^^^^^^^^
[Warning ] Found counter-example:
[Warning ] l: List -> Cons(691483681, Cons(512, Nil()))
[Warning ] e: Int -> -1263292350
[ Info ] Verified: 17 / 19
[ Info ] ┌───────────────────┐
[ Info ] ╔═╡ stainless summary ╞══════════════════════════════════════════════════════════════════════════════════════════════╗
[ Info ] ║ └───────────────────┘ ║
[ Info ] ║ InsertionSort.scala:33:7: buggySortedIns non-negative measure valid U:smt-z3 0,1 ║
[ Info ] ║ InsertionSort.scala:35:5: buggySortedIns body assertion: match exhaustiveness trivial 0,0 ║
[ Info ] ║ InsertionSort.scala:35:5: buggySortedIns postcondition trivial 0,0 ║
[ Info ] ║ InsertionSort.scala:36:21: buggySortedIns postcondition valid U:smt-z3 0,1 ║
[ Info ] ║ InsertionSort.scala:37:38: buggySortedIns postcondition invalid U:smt-z3 0,3 ║
[ Info ] ║ InsertionSort.scala:37:45: buggySortedIns measure decreases valid U:smt-z3 0,1 ║
[ Info ] ║ InsertionSort.scala:37:73: buggySortedIns postcondition invalid U:smt-z3 0,1 ║
[ Info ] ║ InsertionSort.scala:20:7: contents non-negative measure valid from cache 0,0 ║
[ Info ] ║ InsertionSort.scala:20:37: contents body assertion: match exhaustiveness trivial 0,0 ║
[ Info ] ║ InsertionSort.scala:22:24: contents measure decreases valid U:smt-z3 0,0 ║
[ Info ] ║ InsertionSort.scala:25:7: isSorted non-negative measure valid U:smt-z3 0,0 ║
[ Info ] ║ InsertionSort.scala:25:36: isSorted body assertion: match exhaustiveness trivial 0,0 ║
[ Info ] ║ InsertionSort.scala:28:44: isSorted measure decreases valid U:smt-z3 0,1 ║
[ Info ] ║ InsertionSort.scala:15:7: size non-negative measure valid from cache 0,0 ║
[ Info ] ║ InsertionSort.scala:15:34: size body assertion: match exhaustiveness trivial 0,0 ║
[ Info ] ║ InsertionSort.scala:15:34: size postcondition trivial 0,0 ║
[ Info ] ║ InsertionSort.scala:16:19: size postcondition valid U:smt-z3 0,0 ║
[ Info ] ║ InsertionSort.scala:17:25: size postcondition valid U:smt-z3 0,0 ║
[ Info ] ║ InsertionSort.scala:17:29: size measure decreases valid from cache 0,0 ║
[ Info ] ╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
[ Info ] ║ total: 19 valid: 17 (3 from cache, 6 trivial) invalid: 2 unknown: 0 time: 0,81 ║
[ Info ] ╚════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╝
[ Info ] Verification pipeline summary:
[ Info ] cache, anti-aliasing, smt-z3
[ Info ] Shutting down executor service.
Compiling and Executing Examples¶
Scala code written with Stainless library dependencies can be compiled and run using the library sources available on the Stainless github repository, along with the scala compiler and runner script.
See the installation documentation for more information.