David Turner DaveCTurner
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| sdfasdf |
DaveCTurner
/ Leftpad.thy
Last active
June 19, 2023 07:26
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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
/ Blink.thy
Created
June 11, 2021 10:33
Isabelle model of example of dependent specs from https://www.hillelwayne.com/post/spec-composition/
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (* 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
/ EWD840.thy
Last active
March 10, 2021 04:37
Safety and liveness proof of Dijkstra's distributed termination detection algorithm
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| theory EWD840 | |
| imports "HOL-TLA.TLA" | |
| begin | |
| section Utilities | |
| text ‹A handful of general lemmas that were useful along the way.› | |
| lemma temp_impI: | |
| assumes "sigma ⊨ P ⟹ sigma ⊨ Q" |
DaveCTurner
/ Fulcrum.thy
Last active
March 6, 2021 07:07
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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
/ tarsum
Last active
April 8, 2020 16:38
SHA1 hashes of contents of TAR archive without extracting the archive first
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #!/usr/bin/python | |
| import sys | |
| import tarfile | |
| import hashlib | |
| for filename in sys.argv[1:]: | |
| print filename | |
| with tarfile.open(filename, 'r') as tar: | |
| for tarinfo in tar: |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # 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
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| ; | |
| ; twinklies.asm | |
| ; | |
| .include "./m328Pdef.inc" | |
| .dseg | |
| coltable: | |
| .byte 64 |
DaveCTurner
/ MinimumIndex.thy
Last active
April 22, 2018 20:15
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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
/ shard-stats-excerpt.json
Created
April 7, 2018 20:36
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| { | |
| "0": [ | |
| { | |
| "primary": false, | |
| "translog": { | |
| "operations": 1489983, | |
| "size_in_bytes": 1722388686, | |
| "uncommitted_operations": 577877, | |
| "uncommitted_size_in_bytes": 648646336 | |
| }, |
NewerOlder