tobycmurray

#include <stdint.h>
#include <stdlib.h>
#include <stdio.h>

int main(const int argc, const char * argv[]){
  int32_t x, y;
  if (argc < 3){
    fprintf(stderr,"Usage: %s num1 num2\n",argv[0]);
    exit(1);
  }

tobycmurray

theory HoareProcCall
imports Main
begin

typedecl state
typedecl procname
typedecl bexpr

datatype com = Call procname | Skip | Cond bexpr com com

tobycmurray

enum answer {
  GREY,
  YELLOW,
  GREEN
};
typedef enum answer ans;
int choose_ct(int c, int a, int b)
{
  return ((c * a) + ((1 - c) * b));
}