Skip to content

Instantly share code, notes, and snippets.

Dominic Steinhöfel rindPHI

Block or report user

Report or block rindPHI

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
@rindPHI
rindPHI / exportInkscapeLayers.py
Last active Nov 12, 2018
Python script which extracts PDFs from inkscape layers annotated by LaTeX overlay specifications, for the use in LaTeX beamer presentations. The attached SVG file is an example Inkscape SVG for seeing how it works.
View exportInkscapeLayers.py
#!/usr/bin/python3
import xml.etree.ElementTree as ET
import re
import sys
import os
import pyperclip
from pathlib import Path
from subprocess import call
###########################################################################
@rindPHI
rindPHI / firstorder.v
Last active Sep 27, 2018
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"
View firstorder.v
(*
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.
@rindPHI
rindPHI / LLVMParser.g4
Created Aug 24, 2018
ANTLR4 parser for LLVM IR (human readable ASM representation), parser part (lexer is separate)
View LLVMParser.g4
// 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 / LLVMLexer.g4
Created Aug 24, 2018
ANTLR4 parser for LLVM IR (human readable ASM representation), lexer part
View LLVMLexer.g4
// 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 / Main.java
Created Oct 10, 2017
Programmatically using KeY as a program verifier.
View Main.java
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 / Find.java
Last active Jun 29, 2017
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.
View Find.java
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 / Gcd.mps.java
Created May 3, 2017
Gcd method with merge point specifications
View Gcd.mps.java
/*@ 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 / Gcd.java
Created May 3, 2017
Method computing the Greatest Common Divisor (GCD) of two integers
View Gcd.java
/*@ 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 / Main.java
Last active Feb 16, 2017
Example Usage of the Symbolic Execution API
View Main.java
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 / connect-beamer.fish
Created Nov 30, 2016
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.
View connect-beamer.fish
#!/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
You can’t perform that action at this time.