David Turner DaveCTurner

DaveCTurner / gist:371d9b8c95ebb597c5594b93acaaa703

Created September 30, 2024 09:47

Flaps calendar

sdfasdf

DaveCTurner / Blink.thy

Created June 11, 2021 10:33

Isabelle model of example of dependent specs from https://www.hillelwayne.com/post/spec-composition/

	(* Isabelle model of example of dependent specs from https://www.hillelwayne.com/post/spec-composition/ *)

	theory Blink
	imports "./TLA-Utils"
	begin

	definition Blink :: "bool stfun ⇒ action"
	where "Blink v ≡ ACT ($v ⟶ ¬v$ ∧ ¬$v ⟶ v$)"

	definition TurnOn :: "bool stfun ⇒ action"

DaveCTurner / escli.log

Last active April 9, 2019 08:17

Shape with hole

	# see https://discuss.elastic.co/t/failed-to-create-valid-geo-shape/175975

	# ========================================
	# Request:
	PUT /index
	{
	"mappings": {
	"doc": {
	"properties": {
	"parcel": {

DaveCTurner / twinklies.asm

Created April 28, 2018 17:33

DaveCTurner / MinimumIndex.thy

Last active April 22, 2018 20:15

	theory MinimumIndex
	imports Main
	begin

	(* A theory about functions that return the index of a minimum element in a list *)

	(* Correctness properties: any valid implementation instantiates this locale: *)

	locale minimumIndex =
	fixes minimumIndex :: "int list ⇒ nat"

DaveCTurner / Fulcrum.thy

Last active March 6, 2021 07:07

	theory Fulcrum
	imports Main
	begin

	(* https://twitter.com/Hillelogram/status/987432184217731073:
	Fulcrum. Given a sequence of integers, returns the index i that minimizes \|sum(seq[..i]) - sum(seq[i..])\|. Does this in O(n) time and O(n) memory. https://rise4fun.com/Dafny/S1WMn *)

	(* The following merely asserts the time and space bounds. *)

	(* Tail-recursive-modulo-cons calculation of running total - O(n) time and space *)

DaveCTurner / Leftpad.thy

Last active June 19, 2023 07:26

	theory Leftpad
	imports Main
	begin

	definition leftPad :: "'a ⇒ nat ⇒ 'a list ⇒ 'a list"
	where "leftPad padChar targetLength s ≡ replicate (targetLength - length s) padChar @ s"

	definition isPadded :: "'a ⇒ 'a list ⇒ 'a list ⇒ bool"
	where "isPadded padChar unpadded padded ≡ ∃ n. set (take n padded) ⊆ { padChar } ∧ drop n padded = unpadded"

DaveCTurner / shard-stats-excerpt.json

Created April 7, 2018 20:36

DaveCTurner / AllocationBenchmark.java

Created March 9, 2018 09:28

Benchmark of String.join vs stream reduction

	/*
	* Licensed to Elasticsearch under one or more contributor
	* license agreements. See the NOTICE file distributed with
	* this work for additional information regarding copyright
	* ownership. Elasticsearch licenses this file to you under
	* the Apache License, Version 2.0 (the "License"); you may
	* not use this file except in compliance with the License.
	* You may obtain a copy of the License at
	*
	* http://www.apache.org/licenses/LICENSE-2.0

DaveCTurner / Clock.thy

Created February 18, 2018 19:15

Safety, liveness and refinement of simple TLA+ clock specifications in Isabelle/HOL