Archives

Rust Hashers October 20, 2018

A (very bad) hash function in the wild. (Thanks, Wikipedia!)

A hash function, for our purposes here, is a function that takes as input another, general, value, and returns a number that is ideally unique to that value. This number can be used to store the value in an array and then locate it again later without searching the array; in other words, in O(1) time. More or less: there are a lot of other details. For more information, see Rust’s HashMap and various information sources online.

Quote o' the day: Advertising flowers July 28, 2018

How to Live, or a life of Montaigne in one question and twenty attempts at an answer July 25, 2018

Male-pattern baldness and a big mustache.

Ok, so a biography of Michel de Montaigne, a man who invented the essay and examined his own thoughts and reactions, seems a bit like duct-taping a ten-foot pole to another ten-foot pole, but How to Live, or a life of Montaigne in one question and twenty attempts at an answer, by Sarah Bakewell, is not bad. It has its moments, anyway.

The benefits of rain June 26, 2018

The Darker Side May 28, 2018

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

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:

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!

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.

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.

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.

Applied Formal Logic: The bug in Quick Search June 23, 2017

In my last post, I presented a brief introduction to Frama-C and to the process of verifying properties about a very simple C function, a brute force string search. This time around, I intended to do roughly the same thing, using a slightly more complicated function, a faster string searching algorithm. Unfortunately, in doing so, I found a bug in the algorithm. Admittedly, the bug is rather minor and should not affect the actual behavior of an implementation in practice, but still, it is doing something it shouldn’t ought to be doing.

The string searching algorithm I am looking at this time is Quick Search, so named by Daniel M. Sunday in 1990 because it “is a simple, fast, practical algorithm [and] because it can be both coded and debugged quickly” (“A Very Fast Substring Search Algorithm” [PDF]. It is my personal favorite string search because it is, indeed, simple, fast, and practical. Let me quickly show why.

Applied Formal Logic: Brute Force String Search June 19, 2017

Need is there, but tools are not.

– zzz95

Let’s play with Frama-C.

Debunking Economics - Ch. 3: The Demand Curve January 25, 2017

The pain of learning Rust January 19, 2017

I recently saw several posts from ESR discussing his attempts to learn Rust, for use in rewriting NTPsec: “Rust vs. Go” and “Rust severely disappoints me”, as well as “Rust and the limits of swarm design”. These posts gave me the incentive to write down some thoughts I have on the difficulty of approaching Rust. In pariticular, I have noticed are some commonalities among those who have initial difficulties with Rust’s ownership model.

2016 Triangle Pen Show September 2, 2016

Triangle Pen Show 2016

I managed to miss the Atlanta Pen Show this year, but fortunately, I was in North Carolina for the Triangle Pen Show in Cary, June 2-5. It was somewhat smaller and more intimate, but no less fun. Only one room of tables (plus a couple of hallways), but the contents of those tables was no less mind-blowing.

Although I (embarrassingly) never completed the project, I have written before on derivative-based parsing,¹ the work of Matt Might and others. The recent appearance of On the Complexity and Performance of Parsing with Derivatives and a certain immediate interest in parsing re-awakened my curiosity about the subject. (And no, it’s not because Might’s derivative-parsing tool is called Derp (but as an added bonus, the pure recognizer version is “herp” (and the accompanying regular expression package is “rerp”)).²) In this particular post, I would like to demonstrate why I think the technique is cool, by demonstrating that derivative-based regular expressions are cool.

To that end, I’ll start with regular expression matching, then go on to the conversion to a deterministic finite automaton and finally discuss the minor extras needed to build a lexical analyzer, similar to lex or flex (but better).

Quote o' the Day: Age and Syntax Directed Editing July 13, 2016

Laurence Tratt, writing An Editor for Composed Programs, came up with this interesting factoid regarding syntax-directed editing, a bizarre remnant of something horrible that the ’80s have to answer for:

Push-parsing and Pony July 2, 2016

Hey, let’s write a quick parser! A simple one, for the simple version of hoc from The Unix Programming Environment. The chapter on hoc is used to demonstrate the use of the yacc parser; it’s a dandy example to play with parsing.

I haven’t hand written a parser in a long time, so that’s what I want to do now. But there is a bit of a catch: it reads from stdin in Pony. And the interface for that is:

interface StdinNotify
  """
  Notification for data arriving via stdin.
  """
  fun ref apply(data: Array[U8] iso) =>
    """
    Called when data is available on stdin.
    """
    None

  fun ref dispose() =>
    """
    Called when no more data will arrive on stdin.
    """
    None

Quote o' the day: Memory Speed May 23, 2016

This is a quote from Expert C Programming, describing something that I’ve also been complaining about for roughly as long as this book has been in existence. (Remember, it was published in 1994.)

I'm Different May 22, 2016

I’m different!

– Crow T. Robot

Well, lookie here! I’ve done it. I’ve converted this blog from Blogger to a self-hosted Hakyll setup. And it only took several hundred automated Lego ferrets a couple of days.

Ms. Manners' Guide to Excruciatingly Correct Github Pull Requests March 23, 2016

A short guide to academic titles February 25, 2016

Quicksort February 14, 2016

Letterpress cheating in Rust 1.6: How long has it been?!? January 27, 2016

unwrap! January 24, 2016

Another Rust spot: delegation January 21, 2016

A Rust Spot: mmap January 9, 2016

An ode to black humor December 7, 2015

The wisdom o' mcguire November 6, 2015

Ashurbanipal, a text recommendation engine October 6, 2015

A New Thing September 28, 2015

Link o' the day: a couple of DSP links August 22, 2015