Languages specifically designed to make static verification easier

Question

A lot of languages (perhaps all of them) are designed to make writing programs easier. They all have different domains, and aim to simplify developing programs in these domains (C makes developing low-level programs easier, Java makes developing complex business logic easier, et al.). Perhaps other purposes are sacrificed in sake of writing and maintaining programs in an easier, more natural, less error-prone way.

Are there any languages specifically designed to make verification of source code--i.e. static analysis--easier? Of course, capability to write common programs for modern machines should also persist.

Answer 1

One of the design goals of Ada was to support a certian amount of formal verification. It was moderately successful, but verification didn't exactly take off like they were hoping. Luckily Ada is good for far more than that. Sadly, that hasn't helped it much either...

There's an Ada subset called Spark that keeps this alive today. Praxis sells a development suite built around it.

Answer 2

There is SAIL, the Static Analysis Intermediate Language or Flexibo

Answer 3

I haven’t used it myself, so I can’t speak with any authority, but I understand that the Eiffel programming language was designed to use Code by Contracts, which would make static analysis much easier. I don’t know if that counts or not.

Answer 4

Are there any languages specifically designed to make verification of source code easier?

This was a vague goal of both the CLU and ML languages, but the only language design I know that takes static verification really seriously is Spark Ada.

Dijkstra's language of guarded commands (as described in Discipline of Programming) was designed to support static verification, but it was explicitly not supposed to be implemented.

Gerard Holzmann's Promela language was also designed for static analysis by the model checker SPIN, but again it's not executable.

Answer 5

One has two problems in "making verification of source code easier". One is languages in which you don't do gross things such as arbitrary cases (such as C). Another is specifying what you want to verify, for that you need a good assertions languages.

While many languages have proposed such assertions languages, I think the EDA community has been pushing the envelope most effectively with temporal specifications. The "Property Specification Language" is a standard; you can learn more from P1850 Standard for PSL: Property Specification Language (IEEE-1850). One idea behind PSL is that you can add it to existing EDA languages; I think the EDA community has been incorporating into the EDA langauges as time goes by.

I've often wished for something like PSL to embed in conventional computer software.

Answer 6

Auditors in the E language provide a built-in means of writing code analyses within the language itself and requiring that some section of code pass some static check. You might also be interested in the related-work part of the paper.