rindPHI

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;

rindPHI

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)

rindPHI

/*@ 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

rindPHI

/*@ 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;

rindPHI

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.*;

rindPHI

#!/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

rindPHI

Keybase proof

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: