Skip to content
Snippets Groups Projects
memberOf 348 B
Newer Older
memberOf ( x : int , a :[] int | found : bool ) {
    assume #a >= N && #a >=0
        && ( exists k :: 0 <= k && k <# a && a [ k ]= x ) ;
    var k : int {
        k := 0 ;
        found := false ;
        while k <# a do {
Bart Wijgers's avatar
Bart Wijgers committed
            if a [ k ]= x then { found := true } else { skip } ;
Bart Wijgers's avatar
Bart Wijgers committed
}