I hereby claim:
- I am rindphi on github.
- I am dscheurer (https://keybase.io/dscheurer) on keybase.
- I have a public key ASDbCaKb2RPNzwWoQM2nVMThGjDdvA_Wm9nSJ_PCyyJMmgo
To claim this, I am signing this object:
package example; | |
import java.io.File; | |
import java.util.HashMap; | |
import java.util.LinkedList; | |
import java.util.List; | |
import java.util.Set; | |
import org.key_project.util.collection.ImmutableSet; |
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) |
/*@ public normal_behavior | |
@ ensures (a != 0 || b != 0) ==> | |
@ (a % \result == 0 && b % \result == 0 && | |
@ (\forall int x; x > 0 && a % x == 0 && b % x == 0; | |
@ \result % x == 0)); | |
@*/ | |
public static int gcd(int a, int b) { | |
if (a < 0) a = -a; | |
//@ merge_point |
/*@ public normal_behavior | |
@ ensures (a != 0 || b != 0) ==> | |
@ (a % \result == 0 && b % \result == 0 && | |
@ (\forall int x; x > 0 && a % x == 0 && b % x == 0; | |
@ \result % x == 0)); | |
@*/ | |
public static int gcd(int a, int b) { | |
if (a < 0) a = -a; | |
if (b < 0) b = -b; |
package example; | |
import java.io.File; | |
import java.util.HashMap; | |
import java.util.List; | |
import org.key_project.util.collection.ImmutableSLList; | |
import org.key_project.util.java.StringUtil; | |
import de.uka.ilkd.key.control.*; |
#!/usr/bin/fish | |
set fish_greeting | |
function res_x_prompt | |
echo -n 'Please enter the horizontal resolution [1024]: ' | |
end | |
function res_y_prompt | |
echo -n 'Please enter the vertical resolution [768]: ' | |
end |
I hereby claim:
To claim this, I am signing this object: