Skip to content
Snippets Groups Projects
Commit 73837fd7 authored by Viktor Kuncak's avatar Viktor Kuncak
Browse files

counterexamples

parent ff05592f
Branches
Tags
No related merge requests found
import scala.collection.immutable.Set
import funcheck.Annotations._
import funcheck.Utils._
object IntSynth {
def spec(time : Int, m : Int, s : Int) : Boolean = {
require(0 <= time)
time == 60 * m + s &&
0 <= m && 0 <= s && s < 60
}
def f200(m : Int, s : Int) : Boolean = {
!spec(200, m, s)
} holds
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment