Posts tagged "math"
Devanāgarī and mathematical notation October 10, 2007
sigfpe: Monads, Kleisli Arrows, Comonads and other Rambling Thoughts November 6, 2007
Arrows? December 12, 2007
Category Theory vs. General Systems Theory January 28, 2008
Combinator? January 28, 2009
Alfred North Whitehead on notation December 22, 2009
P /= NP, Vinay Deolalikar August 9, 2010
P and NP August 24, 2010
Quote o' the Week: Iversons convention September 2, 2010
Some misconceptions about the CAP Theorem September 29, 2010
Knights, knaves, and Program Construction November 11, 2010
Measured Finger Trees December 11, 2010
Speaking of Peano arithmetic... December 15, 2010
Diagonalization and the Continuum Hypothesis May 27, 2011
Link o' the Day: Markets are Efficient If and Only If P = NP August 24, 2011
Link o' the week: Bayes' Theorem December 2, 2011
Nth Fibonacci number in Emacs Lisp January 29, 2012
Practical regular expression derivatives February 25, 2012
Logicomix May 28, 2012
Quote o' the day: proofs and algorithms June 12, 2012
Turing machines vs. other models of computation October 30, 2014
Abstracted Algebra in Rust July 19, 2015
More Abstracted Algebra in Rust July 28, 2015
Link o' the day: a couple of DSP links August 22, 2015
Applied Formal Logic: Brute Force String Search June 19, 2017
Need is there, but tools are not.
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
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…