Skip to content
Snippets Groups Projects
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)

}