Skip to content
Snippets Groups Projects
Commit 6eb373d4 authored by Régis Blanc's avatar Régis Blanc
Browse files

Proved Linear search is correct

parent 62ede09e
No related branches found
No related tags found
No related merge requests found
import leon.Utils._
object LinearSearch {
def linearSearch(a: Map[Int, Int], size: Int, c: Int, j: Int): Boolean = ({
require(size > 0 && j >= 0 && j < size)
var i = 0
var found = false
(while(i < size) {
if(a(i) == c)
found = true
i = i + 1
}) invariant((if(j < i && !found) a(j) != c else true))
found
}) ensuring(res => (if(!res) a(j) != c else true))
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment