Home

The benefits of rain June 26, 2018

The Darker Side May 28, 2018

“The Darker Side of the ‘Original Affluent Society’”, by David Kaplan…

Read more…

Tutu: an Egyptian god who is more metal than you May 27, 2018

Reading: Why the West Rules---For Now May 26, 2018

From Why the West Rules—For Now: The patterns of history, and what they reveal about the future, by Ian Morris:

Read more…

Software Foundations, Volume 1: Logical Foundations December 8, 2017

There is a certain amount of celebration going on at Maniagnosis’ underground lair at the moment. (Underground lair? There’s nothing underground or lair-ish about this place. It’s not even spectacularly office-like. –Ed) I have (Insert lame drum-roll here.) completed all of the exercises in Software Foundations, Vol. 1: Logical Foundations by Benjamin Pierce, et al. (Very much al.)

(Cue fireworks!) Pop!

Read more…

Quote o' the day: Picking acronyms September 25, 2017

Link o' the day: UTF-8 August 24, 2017

On Complete Gibberish August 15, 2017

Or, Programming language syntax that I don’t like

We interrupt our regularly-scheduled nonsense (Wait! Did someone make up a schedule? Nobody told me! – mcguire) for a brief screed on programming language syntax.

Read more…

Applied Formal Logic: Verifying Quicksort August 9, 2017

Have you ever tried to solve a problem, gotten stuck, backed off, tried again, changed approaches, failed, and then suddenly, with some approach that you’d already abandoned, solved the problem as sweetly as Penelope Doglington begging for part of your sandwich? I’ve had one of those weeks, and now I honestly don’t know what the problem was. Everything seems to be all better now.

So, here it is: my proof of Quicksort. The proof, which is mine, is mine. And therefore, my proof, which belongs to me, is as follows.

Read more…

Applied Formal Logic: Correctness of Quick Search July 16, 2017

When last I left, I had verified that the implementation of Quick Search was safe: the modified algorithm didn’t access memory it shouldn’t, it didn’t have numeric overflows, and it didn’t modify anything outside of its own implementation. And, using Frama-C, the process hadn’t hardly been torturous or even particularly unpleasant at all. The most important tasks were describing the requirements for calling the two functions. Those requirements are…detailed…but nothing more than what an experienced C programmer would have in mind while writing or calling the functions. A final set of shiny set of annotations ensured that the loops and the variable modifications needed by them behaved themselves.

But I hadn’t done anything about proving that the function actually did what it claimed it was supposed to do. It’s not hard to understand (one of the reasons I like Quick Search), but the ANSI/ISO C Specification Language is unfamiliar and I didn’t know how to express what went on, where. Fortunately, Yannick Moy, a software engineer at AdaCore, came to my assistance with an excellent introduction to doing the same thing with SPARK, and Loïc Correnson, one of the creators of Frama-C, popped in with some excellent suggestions (and very flattering comments).

So now, for your software verification pleasure, here is my essay at proving the correctness of Quick Search. It pretty much follows the same pattern as Yannick’s, but I did come up with a slightly different postcondition for make_bad_shift.

Read more…

…or you can find more in the archives.

Dijkstra Knuth OpenAM R REST SAML active directory applied formal logic ashurbanipal authentication books c c++ comics conference continuations coq data structure digital humanities eclipse virgo electronics emacs goodreads haskell http java job ldap link linux lisp math naming nimrod notation osgi parsing pony programming language protocols python quote quotes random ruby rust scala scheme shell software development system administration theory tip toy problems unix vmware yeti
Member of The Internet Defense League
Site proudly generated by Hakyll.