Posts tagged "notation"

Devanāgarī and mathematical notation October 10, 2007

sigfpe: Monads, Kleisli Arrows, Comonads and other Rambling Thoughts November 6, 2007

Arrows? December 12, 2007

Quote o' the day March 21, 2008

Unicode and Japanese e-government April 8, 2008

Apress books July 15, 2008

Gnome does not support US-Dvorak layouts? August 12, 2008

Scala problem #1 January 10, 2009

Combinator? January 28, 2009

Authenticating against an Active Directory Server, pt. 2 September 17, 2009

Alfred North Whitehead on notation December 22, 2009

Einstein's problem December 24, 2009

Phantom Types in Java June 19, 2010

Phantom Types in Java, Revisted July 5, 2010

Link o' the Day: Visual Pedagogy for Internet Protocol Packet Headers July 22, 2010

Subclassing and Java Generics July 31, 2010

Monads and regular expressions August 8, 2010

Quote o' the Week: Iversons convention September 2, 2010

Variations on the theme of monadic regular expressions: Records September 13, 2010

Variations on the theme of monadic regular expressions: Back references September 14, 2010

Some misconceptions about the CAP Theorem September 29, 2010

Subclassing and Java Generics, revisited November 3, 2010

Knights, knaves, and Program Construction November 11, 2010

More Phantom Types in Java December 9, 2010

Equational programming December 25, 2010

Orthogonality January 6, 2011

Tony Morris on static types May 9, 2011

De re profanae May 22, 2011

When Domain Specific Languages Attack! June 4, 2011

Some Lisp suggestions June 17, 2011

Link o' the day: Donald Knuth, Tony Hoare, and goto November 4, 2011

Mad science, abstract data types, and objects December 12, 2011

Link o' the day: Matt Might on parsing with derivatives March 31, 2012

Quote o' the day: proofs and algorithms June 12, 2012

Update to "Mad science, abstract data types, and objects" July 13, 2012

On the definition of object oriented programming July 14, 2012

Rust Iterators February 21, 2013

Creating a Letterpress cheating program in Rust: Traits March 26, 2013

The worst notational abuse October 17, 2013

Abstracted Algebra in Rust July 19, 2015

Quicksort February 14, 2016

A short guide to academic titles February 25, 2016

A deep dive into regular expression derivatives for lexical analysis August 15, 2016

Although I (embarrassingly) never completed the project, I have written before on derivative-based parsing,1 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”)).2) 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).

Read more…

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

Need is there, but tools are not.

– zzz95

Let’s play with Frama-C.

Read more…

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.

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…

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…

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…

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

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

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…

Member of The Internet Defense League
Site proudly generated by Hakyll.