For what it’s worth, it would be easy to make a macro annotation that turns this code:
trait Interface {
@ensures({ res: Int => res >= 0 })
def addNaturals(nats: List[Int]): Int
}
class DynamicImplem extends Interface {
@dynamicChecked
def addNaturals(nats: List[Int]): Int = nats.foldLeft(0)(_ + _)
}
class StaticImplem extends Interface {
@staticChecked
def addNaturals(nats: List[Int]): Int = nats.foldLeft(0)(_ + _)
}
into:
trait Interface {
def addNaturals$contract(nats: List[Int])(res: Int): Boolean = res >= 0
def addNaturals$impl(nats: List[Int]): Int
final def addNaturals(nats: List[Int]): Int = addNaturals$impl(nats)
}
class DynamicImplem extends Interface {
def addNaturals$impl(nats: List[Int]): Int = nats.foldLeft(0)(_ + _) ensuring addNaturals$contract(nats)
}
class StaticImplem extends Interface {
def addNaturals$impl(nats: List[Int]): Int = // whatever syntax is needed to make the static verifier work
}