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:
I hereby claim:
To claim this, I am signing this object:
#!/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 |
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.*; |
/*@ 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; |
/*@ 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 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) |
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; |
// This ANTLR4 lexer grammar is based on the lexer part of an LLVM BNF grammar from | |
// https://gist.github.com/mewmew/a2487392d5519ef49658fd8f84d9eed5, | |
// which in turn has been based on the source code of the official LLVM project, | |
// as of 2018-02-19 (rev db070bbdacd303ae7da129f59beaf35024d94c53). | |
lexer grammar LLVMLexer; | |
LT : '<' ; | |
EQSIGN : '=' ; | |
GT : '>' ; |
// This ANTLR4 parser grammar is based on the parser part of an LLVM BNF grammar from | |
// https://gist.github.com/mewmew/a2487392d5519ef49658fd8f84d9eed5, | |
// which in turn has been based on the source code of the official LLVM project, | |
// as of 2018-02-19 (rev db070bbdacd303ae7da129f59beaf35024d94c53). | |
// * lib/AsmParser/LLParser.cpp | |
// === [ Module ] ============================================================== | |
// https://llvm.org/docs/LangRef.html#module-structure |
(* | |
Compile to PDF with | |
coqc firstorder.v ; coqdoc --latex --no-lib-name -s -p "\usepackage{parskip}\renewcommand{\thesection}{\arabic{section}}" firstorder.v ; pdflatex firstorder.tex | |
*) | |
Require Import Coq.Strings.String. | |
Require Import Coq.Vectors.VectorDef. | |
Require Import Coq.Relations.Relation_Definitions. | |
Module firstorder. |