Channels ▼

Christopher Diggins

Dr. Dobb's Bloggers

Adding a Static Verification Phase to Compiled Languages

March 23, 2008

Many programming languages have a distinct compilation phase and a run-time phase. I propose introducing a new separate phase for static verification.

Programmers want to verify a lot of different properties of their code at compile-time. Some examples are:

  • assuring that type-casts are valid 
  • assuring visibility rules are respected
  • assuring that "constness" or mutability guarantees are maintained
  • assuring that overrides are provided for virtual functions
  • assuring that virtual function hiding is not done implicitly (e.g. in C# using "new" or "virtual")
  • assuring that variables are initialized before used

There are ideas and proposals to check even more things at compile-time in various languages. Some of the examples are:

  •  assuring that class invariants are valid (where it is possible to prove so)
  • checking preconditions and postconditions are legal
  • checking that certain parameters are never null
  • running unit-tests
  • checking that utility and non-utility functions, are valid.

Many of these tasks are verifications that can be performed at run-time in a language that supports introspection or reflection. The problem with adding introspection is that it somewhat inhibits the compiler's ability to optimize code: it has to maintain a complete representation of the code just for examination.  The other problem is that this verification doesn't need to be done at run-time, it only needs to be done by the developer, so there is an undue performance hit if we run all of the code during every execution. One solution is to turn on and off the verification part of the code using pragmas or macros, but the compiler has no sense whether we want to generate the abstract representation of the code.

I propose that instead of implicitly performing many of these checks that a language should provide the facilities (introspection) and libraries (such as a theorem prover) for verifying the various properties of code. This would be done in a separate verification phase that occurs immediately after compilation. The verification phase would be like running a separate program woven into your main program, which has complete read-only access to the abstract syntax tree.

What do you think of this idea? Would you like to have better control over verifying the static properties of your code? Do you think it would encourage better programming practices such as unit-testing, and usage of programming contracts? What could you do with this kind of reflection in a language like C++, that you can't do now?

Related Reading


More Insights






Currently we allow the following HTML tags in comments:

Single tags

These tags can be used alone and don't need an ending tag.

<br> Defines a single line break

<hr> Defines a horizontal line

Matching tags

These require an ending tag - e.g. <i>italic text</i>

<a> Defines an anchor

<b> Defines bold text

<big> Defines big text

<blockquote> Defines a long quotation

<caption> Defines a table caption

<cite> Defines a citation

<code> Defines computer code text

<em> Defines emphasized text

<fieldset> Defines a border around elements in a form

<h1> This is heading 1

<h2> This is heading 2

<h3> This is heading 3

<h4> This is heading 4

<h5> This is heading 5

<h6> This is heading 6

<i> Defines italic text

<p> Defines a paragraph

<pre> Defines preformatted text

<q> Defines a short quotation

<samp> Defines sample computer code text

<small> Defines small text

<span> Defines a section in a document

<s> Defines strikethrough text

<strike> Defines strikethrough text

<strong> Defines strong text

<sub> Defines subscripted text

<sup> Defines superscripted text

<u> Defines underlined text

Dr. Dobb's encourages readers to engage in spirited, healthy debate, including taking us to task. However, Dr. Dobb's moderates all comments posted to our site, and reserves the right to modify or remove any content that it determines to be derogatory, offensive, inflammatory, vulgar, irrelevant/off-topic, racist or obvious marketing or spam. Dr. Dobb's further reserves the right to disable the profile of any commenter participating in said activities.

 
Disqus Tips To upload an avatar photo, first complete your Disqus profile. | View the list of supported HTML tags you can use to style comments. | Please read our commenting policy.
 


Video