Home

The case for Semantic Analysis

How to statically ensure software reliability is aimed mostly at C programmers in the embedded space:

The term semantic analysis refers to a group of advanced static analysis techniques that enable users to detect runtime and/or dynamic errors in software applications.

There is a conspicuous silence in the article on how PLs might help the tools. And I can't help but think that the static semantic analysis amounts to Constraint Programming (propagate and branch).

By Chris Rathman at 2006-05-11 17:51 | Software Engineering | other blogs | 7417 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Contracts

From a PL-support perspective, it seems like this semantic analysis technique would be made more tractable by having provision for adding (statically-checkable) contracts (ala SPARK Ada or ESC2/Java) to the source code. That would permit the use of semantic analysis to ensure that individual contracts for low-level routines are fulfilled, and compositional reasoning on contracts to ensure that high-level safety specs are met. Of course, that approach is probably what SPARK and ESC2 already use...

By Allan McInnes at Thu, 2006-05-11 19:21 | login or register to post comments

Contracts would narrow it down...

...though if you look at many of the languages that use contracts, the contract is something which can be disabled, so it would only work if you consciously kept them in place after delivery. Also, the contracts would have to be statically analyzed to determine whether you can ensure that they will not produce a runtime error - the contracts are a runtime assertion - you can say that a contract will always be enforced, but you can't guarantee that someone will not try to violate the contract.

By Chris Rathman at Thu, 2006-05-11 19:58 | login or register to post comments

Compile-time contracts

I was thinking more of compile-time contracts, rather than run-time contracts. Something that would make the anaylsis of large programs more tractable, by reducing the amount of semnantic analysis that needs to be done.

For example, using the 1/(x-y) example from the article, you might have a contract with a pre-condition that specifies a range of values for x and y. Then the semantic analysis only needs to examine that range of values, rather than the whole set of Ints. Similarly, you might have post-conditions on the functions that provide values for x and y, and use semantic analysis to ensure that those post-conditions are met. Correctness of the composition of those functions can then be checked by ensuring that the pre and post conditions match, instead of having to check the the full semantics of the composite function. The result would be akin to type inference and static type-checking, but able to check things at a finer level of granularity.

Edit: ESC/Java apparently does some of this kind of thing - this presentation includes a simple example.

By Allan McInnes at Thu, 2006-05-11 21:30 | login or register to post comments

Nemerle

The Nemerle guys want to integrate the Spec# theorem prover into their compiler as well, which would be very cool. Actually every time I read about Nemerle I like it more, but right now they're just compiled to runtime assertions.

By Mike Hearn at Fri, 2006-05-12 11:26 | login or register to post comments

silence

There is a conspicuous silence in the article on how PLs might help the tools.

Well, it's written by a consultant & a marketing person of a company that makes a tool that analyzes only C programs. Their aim is to keep people writing in C and sell the tool.

By Koray Can at Thu, 2006-05-11 19:23 | login or register to post comments

consent

Perhaps that might be because there are lots of C compilers for embedded architectures, and a notable lack of compilers for other programming languages.

By Eric Brown at Mon, 2006-05-15 17:40 | login or register to post comments

C?

Why don't we just write in assembly instead, and do semantic anaylsis on that :P

Since I'm already pessimistic today... I'll go ahead and say that in my recent embedded project, 80% of our s/w bugs have been due to poor specification or bugs in the components we interface with. I'd prefer some more runtime-analysis tools, thank you very much :)

By Steven Hugg at Fri, 2006-05-12 02:17 | login or register to post comments

Off the top of my head...

Explicit static typing
Explicit module boundaries and access controls
Limits (but not prohibitions) on mutable state
Message-passing concurrency
Explicit error handling
Design-By-Contract

A statically-typed version of Erlang with Design-By-Contract support would by just about optimal for semantic analysis, as well as being great for building highly manageable products.

By Dave Griffith at Fri, 2006-05-12 13:12 | login or register to post comments

Erlang++?

I think I'd heard that the Dialyzer has been put to awfuly good use? (I certainly didn't like part in the Erlang video where they found a spelling mistake had caused their runtime error.)

By raould at Mon, 2006-05-15 19:59 | login or register to post comments