Skip to content

Instantly share code, notes, and snippets.

View rindPHI's full-sized avatar

Dominic Steinhöfel rindPHI

26 followers · 9 following
View GitHub Profile
@rindPHI
rindPHI / keybase.md
Created July 15, 2016 07:32

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:

@rindPHI
rindPHI / connect-beamer.fish
Created November 30, 2016 08:17
An interactive script for the fish shell, managing the connection to connected screens / beamers especially in cases where the beamer is not recognized, and therefore the normal (graphical) system configuraion tools fail.
#!/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
rindPHI / Main.java
Last active February 16, 2017 13:39
Example Usage of the Symbolic Execution API
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
rindPHI / Gcd.java
Created May 3, 2017 13:00
Method computing the Greatest Common Divisor (GCD) of two integers
/*@ 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
rindPHI / Gcd.mps.java
Created May 3, 2017 13:09
Gcd method with merge point specifications
/*@ 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
rindPHI / Find.java
Last active June 29, 2017 09:32
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.
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
rindPHI / Main.java
Created October 10, 2017 11:20
Programmatically using KeY as a program verifier.
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
rindPHI / LLVMLexer.g4
Created August 24, 2018 12:41
ANTLR4 parser for LLVM IR (human readable ASM representation), lexer part
// 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 : '>' ;
@rindPHI
rindPHI / LLVMParser.g4
Created August 24, 2018 12:42
ANTLR4 parser for LLVM IR (human readable ASM representation), parser part (lexer is separate)
// 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
@rindPHI
rindPHI / firstorder.v
Last active September 27, 2018 16:52
An attempt to define the syntax and semantics of a predicate logic language, with a theorem on conservativity of structure extension. It's a failed attempt, therefore it contains "challenges". If somebody knows how to resolve them -- please let me know"
(*
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.