-
Etienne Kneuss authoredEtienne Kneuss authored
Array3.scala 284 B
/* Copyright 2009-2013 EPFL, Lausanne */
import leon.Utils._
object Array3 {
def foo(): Int = {
val a = Array.fill(5)(3)
var i = 0
var sum = 0
(while(i < a.length) {
sum = sum + a(i)
i = i + 1
}) invariant(i >= 0)
sum
} ensuring(_ == 15)
}