Can new software testing frameworks bring us to provably correct software?

By Matthew Heusser, CIO |  Software

If we could define our software in a precise, clear way, it may be possible to take that definition and transform it, over a series of steps, into the actual program. This turns out to be remarkably similar to what a compiler does--and compilers can, in theory, be demonstrated as correct.

This technique is sometimes called transformational specification. Its challenge: That precise definition will need to be interpreted by some sort of program. In order to make the specification precise, it needs to be written in code, and that code will probably have errors.

How-to: Software Testing Lessons Learned From Knight Capital Fiasco

As an academic discipline, the formal specification for finding the largest element in an array of integers requires roughly 600 small transformations, expressed in predicate calculus. That is complex enough that a graduate student in computer science might write a transform to, say, add up the change in your pocket or sort and count it, but it can't be used for practical software development.

Behavior-Driven Development: Code That Looks Like English

Like transformational specification, behavior driven development (BDD) also separates the spec from the code. Like its older cousin, BDD begins by writing examples of what the software will do in high-level language that looks more like English than most traditional code.

Here's an example in Given/When/Then format:

Given a logged-in user

When I add item 12345 into my shopping cart

And I click order

Then I see the order screen with item 12345

To implement this, the transformational program would need to know what the shopping cart is, what logged in means, what the order button is and so on. These types of Given/When/Then statements can be very valuable and can be compiled, with a human coming along afterward to define the keywords "shopping cart," "logged in" and so on.

Tips: Stupid QA Tricks: Colossal Software Testing Oversights

These examples (but not a programmatic spec), defined up front, mean the programmer can know that, if he delivers the code to acceptance test and it meets some minimum standards of quality, then the code can "work" under precise condition. In some cases, the checks can run automatically with every build, so the build system can find some major regression errors immediately after commit.

Model-Based Testing: Intelligent Automation for Big, Obvious Errors


Originally published on CIO |  Click here to read the original story.
Join us:
Facebook

Twitter

Pinterest

Tumblr

LinkedIn

Google+

Spotlight on ...
Online Training

    Upgrade your skills and earn higher pay

    Readers to share their best tips for maximizing training dollars and getting the most out self-directed learning. Here’s what they said.

     

    Learn more

SoftwareWhite Papers & Webcasts

Webcast On Demand

Next Generation Firewall

Sponsor: PC Connection

See more White Papers | Webcasts

Answers - Powered by ITworld

ITworld Answers helps you solve problems and share expertise. Ask a question or take a crack at answering the new questions below.

Join us:
Facebook

Twitter

Pinterest

Tumblr

LinkedIn

Google+

Ask a Question