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
 Quote o' the day: Questions which ought not to be asked May 7, 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.
– zzz95
Let’s play with FramaC.
Read more… 
Applied Formal Logic: The bug in Quick Search June 23, 2017
In my last post, I presented a brief introduction to FramaC 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…