Last active
June 29, 2017 09:32
-
-
Save rindPHI/c0bf00c371e9491a7598840ec5063f91 to your computer and use it in GitHub Desktop.
A method finding an element in an integer array, returning -1 if the element has not been found. The source code includes the JML specification covering all facts that our strength analysis tool discovered.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
public class Find { | |
//@ ghost int f_iLastRun; | |
// Everything covered | |
/*@ public normal_behavior | |
@ ensures | |
@ ((\exists int i; i >= 0 && i < arr.length; arr[i] == n) ==> | |
@ (arr[\result] == n && \result == f_iLastRun) | |
@ ) | |
@ && ((\forall int i; i >= 0 && i < arr.length; arr[i] != n) ==> \result == -1) | |
@ ; | |
@ assignable f_iLastRun; | |
@*/ | |
public int find(int[] arr, int n) { | |
int i = 0; | |
int result = -1; | |
//@ set f_iLastRun = i - 1; | |
/*@ loop_invariant | |
@ i >= 0 && i <= arr.length | |
@ && i == f_iLastRun + 1 | |
@ && (result != -1 || (\forall int k; k >= 0 && k < i; arr[k] != n)) | |
@ && (result == -1 || arr[result] == n && result == i-1) | |
@ ; | |
@ decreases arr.length - i; | |
@ assignable f_iLastRun; | |
@*/ | |
while (result == -1 && i < arr.length) { | |
//@ set f_iLastRun = i; | |
if (arr[i] == n) { | |
result = i; | |
} | |
i++; | |
} | |
return result; | |
} | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment