jorendorff

// A brief formalization of context-free grammars in Dafny.

// Terminals (i.e. tokens).
type T = string

// Names of nonterminals.
type Nt = string

// The right-hand side of a production is a sequence of terminals and nonterminals.
datatype Symbol = T(T) | Nt(Nt)

jorendorff

predicate sorted<T>(le: (T, T) -> bool, s: seq<T>)
{
  forall i, j :: 0 <= i <= j < |s| ==> le(s[i], s[j])
}

predicate hasSameElements<T>(a: seq<T>, b: seq<T>)
{
  multiset(a) == multiset(b)
}

jorendorff

Destroying the universe

Hi everyone, this talk is called "Destroying the Universe", for reasons that will become obvious...

Stop me if you've heard this one. Once there were five people who lived in five houses. I know this picture only shows four houses... But I had a boss once who said that there's some sort of rule,

jorendorff

// insertion_sort.dfy - An attempt to verify a simple O(n^2) insertion sort implementation

predicate sorted(a: seq<nat>)
{
  forall j, k :: 0 <= j < k < |a| ==> a[j] <= a[k]
}

// Find the point where a[i] could be inserted into a[..i] to keep it sorted.
//
// This could be switched to binary search without changing the signature,

jorendorff

// *** Arrays that are all zeroes

predicate all_zeroes_up_to(a: array<nat>, stop: nat)
  reads a
  requires 0 <= stop <= a.Length
{
  forall i :: 0 <= i < stop ==> a[i] == 0
}

predicate all_zeroes(a: array<nat>)

jorendorff

#!/usr/bin/env python3

import sys, os, time
import math, random
import functools

PALETTE = ' .+?#$%'

DEFAULT_WIDTH = 160

jorendorff

changeset:   473589:4afcb87593a5
tag:         tip
user:        Jason Orendorff <[email protected]>
date:        Tue Apr 17 14:12:42 2018 +0200
summary:     Bug 1454613 - Build binsource when building SpiderMonkey

diff --git a/js/src/frontend/binsource/Cargo.toml b/js/src/frontend/binsource/Cargo.toml
--- a/js/src/frontend/binsource/Cargo.toml
+++ b/js/src/frontend/binsource/Cargo.toml
@@ -6,8 +6,12 @@ authors = ["David Teller <D.O.Teller@gma

jorendorff

Beer cheese bread

(from: Better Homes and Gardens New Cook Book, 1996)

1. Set oven to 375°F. Grease the bottom and sides of an 8×4×2-inch or 9×5×3-inch loaf pan; set aside.

2. In a large mixing bowl, stir together:

   • 2½ cups flour
   • 2 tbsp sugar

• 2½ tsp baking powder

jorendorff

	.section	__TEXT,__text,regular,pure_instructions
	.macosx_version_min 10, 13
	.section	__TEXT,__literal8,8byte_literals
	.p2align	3
LCPI0_0:
	.quad	4742290407621132288     ## double 1073741824
LCPI0_1:
	.quad	4741671816366391296     ## double 1.0E+9
LCPI0_11:
	.quad	4472074429978902528     ## double 9.3132257461547852E-10

jorendorff

~/play/sine/timings$ make
c++ -O2 -std=c++11   -c -o clock_gettime.o clock_gettime.cc
c++ -O2 -std=c++11   -c -o lib.o lib.cc
c++ -O2 -std=c++11  clock_gettime.o lib.o -o clock_gettime
c++ -O2 -std=c++11   -c -o fwrite.o fwrite.cc
c++ -O2 -std=c++11  fwrite.o lib.o -o fwrite
c++ -O2 -std=c++11   -c -o mutex.o mutex.cc
c++ -O2 -std=c++11  mutex.o lib.o -o mutex
c++ -O2 -std=c++11   -c -o time-delta.o time-delta.cc
c++ -O2 -std=c++11  time-delta.o lib.o -o time-delta