Posts tagged "software development"

Requirements... February 6, 2008

Some [More] Notes on the Abstraction Penalty for IA86 C++ Compilers February 25, 2008

Functional Programming in the ACM CS Curriculum July 9, 2008

Finally! July 24, 2008

Will the real whiteboard pattern stand up? July 29, 2008

OSGi vs. Log4j August 12, 2008

Just so wrong... August 21, 2008

OSGi vs. JRuby on Rails, pt. 1 December 7, 2008

OSGi vs. JRuby on Rails, pt. 2 December 8, 2008

JRuby already has OSGi metadata December 11, 2008

Scala problem #1 January 10, 2009

Adobe Flex Messaging (or BlazeDS) Vs. OSGi March 25, 2009

Steve Vinoski, REST, and distributed systems June 20, 2009

HTTPS Virtual Hosts in Apache July 2, 2009

API design and granfalloons July 9, 2009

GNU Screen July 9, 2009

Brilliant make rule July 20, 2009

Running JRuby in an OSGi container July 24, 2009

Interface idiocy: When is returning an empty List not good enough? March 15, 2010

Requiescat in Pace: SpringSource dm Server June 6, 2010

Phantom Types in Java June 19, 2010

Quote o' the Week: Christopher Alexander June 24, 2010

Phantom Types in Java, Revisted July 5, 2010

Link o' the Day: Beej! July 24, 2010

Monads and regular expressions August 8, 2010

Quote o' the Week: It’s [Not] Faster Because It’s C October 12, 2010

Link o' the Day: Top 10 Performance Problems October 17, 2010

Subclassing and Java Generics, revisited November 3, 2010

Knights, knaves, and Program Construction November 11, 2010

Finger Trees November 25, 2010

Measured Finger Trees December 11, 2010

Equational programming December 25, 2010

Orthogonality January 6, 2011

What Every Computer Scientist Should Know About Floating-Point Arithmetic January 28, 2011

The one problem with open source February 1, 2011

If I Only Changed the Software, Why Is the Phone on Fire? March 11, 2011

A few more comments about ...Why Is the Phone on Fire? March 14, 2011

SQL Combinators in Java April 13, 2011

There are limits to what you can do in the child process. May 2, 2011

Tony Morris on static types May 9, 2011

De re profanae May 22, 2011

Quote o' the Day: Software Awesomeness June 3, 2011

Some Lisp suggestions June 17, 2011

The Tappan Zee Bridge and software development August 19, 2011

Why I usually prefer the GPL October 24, 2011

Oracle JDBC API changes: things that make me sigh October 28, 2011

Systems programming November 1, 2011

Consolidated Reference List for the IEEE Software Engineering Body of Knowledge November 21, 2011

Consolidated Reference List for the Software Engineering Body of Knowledge, Pt. 2 November 24, 2011

Tip: Converting a CVS repository to git December 30, 2011

Quote o' the week: Don Stewart on the big picture February 3, 2012

Link o' the day: Java and memory February 9, 2012

The Clean Coder March 18, 2012

ASON March 27, 2012

Quote o' the day: OMG! Something from Steve Yegge! May 18, 2012

On the definition of object oriented programming July 14, 2012

Tom DeMarco on project control July 18, 2012

Link o' the day: Brian Kernighan on the Elements of Programming Style April 28, 2013

mmap and the Rust Foreign Function Interface June 12, 2013

A faster hashmap in Rust October 12, 2013

Best of mcguire: ruthless simplicity April 19, 2014

If you have a problem and you think, I'll use sed... June 7, 2014

Quote o' the day: On the use of ducks June 26, 2014

One stupid shell scripting trick everyone should know April 11, 2015

Reimplementing ashurbanipal.web in Rust July 14, 2015

Quicksort February 14, 2016

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

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:

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…

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