Programming with correctness guarantees

Programming with correctness guarantees

[oleg]

Andrej Bauer wrote:
> I would go further: it would be interesting to augment real programming
> languages with ways of writing specifications that can then be tackled
> by theorem provers and proof asistants.

Has been done, to a good effect. The following are three examples,
which use quasi-comments to add various correctness propositions to the
existing programming language. The first example, SPARK, has been used
for *large*, industrial projects, for quite some time.

@Book{		barnes-high,
  author	= "John Barnes",
  title		= "High Integrity Software: 
                    The {SPARK} Approach to Safety and Security",
  booktitle	= "High Integrity Software: 
                    The {SPARK} Approach to Safety and Security",
  year		= 2003,
  url		= "http://www.praxis-his.com/sparkada/sparkbook.asp 
                   http://www.praxis-his.com/sparkada/pdfs/sampler_final.pdf",
  isbn		= "0-321-13616-0",
}
The sample chapter is quite good.

@TechReport{	hunt-singularity,
  author	= "Galen Hunt and James R. Larus and Mart{\'\i}n Abadi and 
        Mark Aiken and Paul Barham and Manuel F{\"a}hndrich and
        Chris Hawblitzel and Orion Hodson and Steven Levi and
        Nick Murphy and Bjarne Steensgaard and David Tarditi and
        Ted Wobber and Brian D. Zill",
  title		= "An Overview of the {S}ingularity Project",
  year		= 2005,
  month		= oct,
  number	= "MSR-TR-2005-135",
  url		= "http://research.microsoft.com/research/pubs/view.aspx?type=technical+report&id=989",
  abstract = "Singularity is a research project in Microsoft Research
that started with the question: what would a software platform look
like if it was designed from scratch with the primary goal of
dependability? Singularity is working to answer this question by
building on advances in programming languages and tools to develop a
new system architecture and operating system (named Singularity), with
the aim of producing a more robust and dependable software
platform. Singularity demonstrates the practicality of new
technologies and architectural decisions, which should lead to the
construction of more robust and dependable systems.",
}

@Misc{		kieburtz-p-logic,
  author	= "Richard B. Kieburtz",
  title		= "{P}-Logic: Property Verification for {H}askell Programs",
  year		= 2002,
  month		= "14~"  # aug,
  url		= "ftp://ftp.cse.ogi.edu/pub/pacsoft/papers/Plogic.pdf"
}

Why this isn't widespread? Certainly Praxis doesn't seem to complain
too much about that fact: they can charge basically anything they
want, given little competition. I remember reading somewhere that
after a division of Siemens applied this technique to a high assurance
project, they noted an exhilarating feeling of being able to program
without unit tests. The code was correct by construction.

Re: Programming with correctness guarantees

[Andrej Bauer]

Dear Oleg,

thank you for the references. This is very useful and I will take the 
references into account in the project with Chris Stone, see 
http://math.andrej.com/rz. Our tool is slanted towards specification 
construction (not verification) from mathematical defintions. We plan to 
use it for real number computation and computable mathematical analysis.

In fact, I think Chris mentioned SPARK the other day and how we should 
have a look at it.

Best regards,

Andrej

Re: [Caml-list] Re: Programming with correctness guarantees

[Chris King]

You may also be interested in Why (http://why.lri.fr/).  It is an
ML-ish language which allows pre- and postconditions to be specified
and translates those assertions into input to a variety of proof
engines (such as the proof assistant Coq or the decision procedure
Simplify).  You can then extract your code as O'Caml.

- Chris King

Re: [Caml-list] Programming with correctness guarantees

[Joshua D. Guttman]

oleg@pobox.com writes:

>   I remember reading somewhere that after a division of
>   Siemens applied this technique to a high assurance
>   project, they noted an exhilarating feeling of being
>   able to program without unit tests. The code was correct
>   by construction.

This seems really frightening.  Don't the unit tests also
serve another purpose, namely to confirm that the formal
model of the software environment is correct?

That is, that all of the libraries you're linking against
(and the compiler itself) are behaving in a way that matches
the expectations you formalized?

As well as a concrete confirmation that the formalized ideas
match correctly against what you really wanted in specific
instances:  the formal insight of human beings is imperfect.
(:-) 

I hope that the words "exhilarating feeling" were meant to
indicate that they didn't really do this, but had the
impression that they could *almost* do so.  

You don't want to lose contact with the real world
constraints when programming in a formally supported way.

I suppose that this doesn't really have much to do with
OCaml; apologies.  

        Joshua 


-- 
	Joshua D. Guttman 
	The MITRE Corporation

Re: [Caml-list] Programming with correctness guarantees

[Jean-Christophe Filliatre]

Joshua D. Guttman writes:
 > oleg@pobox.com writes:
 > 
 > >   I remember reading somewhere that after a division of
 > >   Siemens applied this technique to a high assurance
 > >   project, they noted an exhilarating feeling of being
 > >   able to program without unit tests. The code was correct
 > >   by construction.
 > 
 > This seems really frightening. 

There's a joke around in the formal methods community: ``would you
prefer to get on a plane whose software has been proved correct or
has been tested?''

More seriously, I heard a similar remark from a French company which
formally verified the embedded code of an automatic subway line (using
the B method). They explained that, after the verification had been
completed, the unit phase was not suppressed, but greatly reduced.

-- 
Jean-Christophe

Re: [Caml-list] Programming with correctness guarantees

[Robert Fischer]

What, exactly, is the difference between a unit test and formal
verification of an application?  I've long been under the opinion that
Design-by-Contract is just a way to write unit tests quickly -- after all,
you write something that looks kinda like code, attach it to something we
arbitrarily define as a "unit", run some framework on that, and the
framework tells you if something violates those rules.  This sounds like
unit testing to me.

Now, I could be wrong, and there could be something obvious I'm missing,
and I'd like to know if there is -- but it just doesn't seem like there's
anything like a clear line between unit tests and program verification.

Given that there isn't, it seems like people writing verified code aren't
really skipping the unit testing phase at all: they're just doing unit
testing in a funny way.

~~ Robert Fischer.
Fischer Venture Management Corporation

On Thu, February 1, 2007 2:12 pm, Jean-Christophe Filliatre wrote:
>
> Joshua D. Guttman writes:
>  > oleg@pobox.com writes:
>  >
>  > >   I remember reading somewhere that after a division of
>  > >   Siemens applied this technique to a high assurance
>  > >   project, they noted an exhilarating feeling of being
>  > >   able to program without unit tests. The code was correct
>  > >   by construction.
>  >
>  > This seems really frightening.
>
> There's a joke around in the formal methods community: ``would you
> prefer to get on a plane whose software has been proved correct or
> has been tested?''
>
> More seriously, I heard a similar remark from a French company which
> formally verified the embedded code of an automatic subway line (using
> the B method). They explained that, after the verification had been
> completed, the unit phase was not suppressed, but greatly reduced.
>
> --
> Jean-Christophe
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>

Re: [Caml-list] Re: Programming with correctness guarantees

[Jean-Christophe Filliatre]

Chris King writes:
 > You may also be interested in Why (http://why.lri.fr/).  It is an
 > ML-ish language which allows pre- and postconditions to be specified
 > and translates those assertions into input to a variety of proof
 > engines (such as the proof assistant Coq or the decision procedure
 > Simplify).  You can then extract your code as O'Caml.

Many thanks for the advertisement :-)

But before anybody rushes to download it, I want to say that the Why
tool mostly borrows ML syntactic constructs, but is far from being a
language to specify and verify real ML programs. 

It is actually rather some kind of WHILE language, without aliasing,
that we use as an intermediate language to do verification of (real,
this time) C and Java programs, through suitable models of pointers
and memory layout.

Specifying and verifying real ML programs is currently ongoing
work in many research teams and there is no doubt we'll eventually
be able to formally verify Ocaml programs.

-- 
Jean-Christophe

Re: [Caml-list] Programming with correctness guarantees

[Jacques Carette]

Jean-Christophe Filliatre wrote:
> There's a joke around in the formal methods community: ``would you
> prefer to get on a plane whose software has been proved correct or
> has been tested?''
>   
I heard, from someone working on an automated train system, that 
everyone working on the system was required to be on the inaugural run 
of said train.

I would trust such "people methods" even more than proof and testing!

Jacques

Re: [Caml-list] Programming with correctness guarantees

[Jean-Christophe Filliatre]

Robert Fischer writes:
 > What, exactly, is the difference between a unit test and formal
 > verification of an application? 

(I hope I don't misunderstand what you mean by "formal verification" here)

At least in its deductive form (i.e. frameworks similar to Hoare
logic), formal verification interprets a program and its specification
as a mathematical formula whose validity implies  the program
correctness. This formula usually includes universal quantifiers, and
thus can only be proved using some logical reasoning, but not testing.

If we consider for instance the following Ocaml code

	let min x y = if x <= y then x else y

and the (incomplete) specification ``forall x y, min x y <= x'' then
the correctness is equivalent to the following formula:

        forall x y, (x <= y implies x <= x) and (x > y implies y <= x)

This is a statement easily established by most automatic provers. Then
there is no need testing function min anymore, since it has been
proved correct for _any_ input values.

-- 
Jean-Christophe

Re: [Caml-list] Programming with correctness guarantees

[Bob Williams]

On Thu, Feb 01, 2007 at 03:43:04PM -0500, Jacques Carette wrote:
> Jean-Christophe Filliatre wrote:
> >There's a joke around in the formal methods community: ``would you
> >prefer to get on a plane whose software has been proved correct or
> >has been tested?''
> >  
> I heard, from someone working on an automated train system, that 
> everyone working on the system was required to be on the inaugural run 
> of said train.
> 
> I would trust such "people methods" even more than proof and testing!
> 
> Jacques

This reminds me of the Roman Empire system: the first person to cross
a new bridge was the engineer who built it!

Re: [Caml-list] Programming with correctness guarantees

[skaller]

On Thu, 2007-02-01 at 21:57 +0100, Jean-Christophe Filliatre wrote:

> This is a statement easily established by most automatic provers. Then
> there is no need testing function min anymore, since it has been
> proved correct for _any_ input values.

This isn't right, IMHO: there is still need to test: 
after all the proof itself, and the theorem prover,
the operating system, etc, all introduce additional risks.

The point is that you no longer rely solely on the WORST
possible way of guessing if a program is going to work: testing.
Instead you rely on BOTH proof and testing, and you can put
a lot more effort (money) into the proof than the testing
to get the best results. But you never forget to actually test
the code too!

Don't forget that even with perfect machine model .. the actual
specification may be wrong! Correctness isn't enough! The program
has to actually work! But now, you can more easily blame the
spec writer than the programmer if it doesn't ... :)

-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] Programming with correctness guarantees

[Jean-Christophe Filliatre]

 > > it would be interesting to augment real programming
 > > languages with ways of writing specifications that can then be tackled
 > > by theorem provers and proof asistants.

Some readers of this thread may be interested by the following proof
of an OCaml implementation of Peterson's algorithm by Tom Ridge:

http://www.cl.cam.ac.uk/~tjr22/doc/concTalk20070124.pdf

-- 
Jean-Christophe

Re: [Caml-list] Programming with correctness guarantees

[Tom]

[-- Attachment #1: Type: text/plain, Size: 245 bytes --]

SML is a programming language wit a formal proof of semantics.

I prefer OCaml for it's good implementation - however good a proof, if the
programmer screwed up, or something simply got into way, the end product is
flawed.

Just my two cents...

[-- Attachment #2: Type: text/html, Size: 268 bytes --]

Design-by-contract and Type inference?

[David MENTRE]

Hello Oleg,

oleg@pobox.com writes:

> @Book{		barnes-high,
>   author	= "John Barnes",
>   title		= "High Integrity Software: 
>                     The {SPARK} Approach to Safety and Security",
[...]
> @TechReport{	hunt-singularity,
>   author	= "Galen Hunt and James R. Larus and Mart{\'\i}n Abadi and 
>         Mark Aiken and Paul Barham and Manuel F{\"a}hndrich and
>         Chris Hawblitzel and Orion Hodson and Steven Levi and
>         Nick Murphy and Bjarne Steensgaard and David Tarditi and
>         Ted Wobber and Brian D. Zill",
>   title		= "An Overview of the {S}ingularity Project",

Thank you for those interesting pointers. Interestingly both Spark
language and Sing# language used in Singularity contains
Design-by-Contract-like features (pre- and post-conditions, invariants,
...). 

Does anybody know if there is research on design-by-contract (as used in
Eiffel or Spark) and type inference (as used in OCaml)? For example,
relationships between both mechanisms, how the compiler could infer
contracts for a sub-class of a class, how contracts can be maintained
with minimal work from the programmer (a very useful property of ML type
inference), how contract can be statically checked using type inference
information, etc.

Best wishes,
d.
-- 
GPG/PGP key: A3AD7A2A David MENTRE <dmentre@linux-france.org>
 5996 CC46 4612 9CA4 3562  D7AC 6C67 9E96 A3AD 7A2A

Re: [Caml-list] Design-by-contract and Type inference?

[Benedikt Grundmann]

[-- Attachment #1: Type: text/plain, Size: 2201 bytes --]

Hello

Well a lot of the stuff you express with DBC can be expressed using
dependent types (Array indices are a popular example).  You should take that
in account in your search for papers (If I recall correctly there are quite
a few papers on combining dependent types and (at the very least
partial/local) type inference).

Cheers,

Bene

2007/2/4, David MENTRE <dmentre@linux-france.org>:
>
> Hello Oleg,
>
> oleg@pobox.com writes:
>
> > @Book{                barnes-high,
> >   author      = "John Barnes",
> >   title               = "High Integrity Software:
> >                     The {SPARK} Approach to Safety and Security",
> [...]
> > @TechReport{  hunt-singularity,
> >   author      = "Galen Hunt and James R. Larus and Mart{\'\i}n Abadi and
> >         Mark Aiken and Paul Barham and Manuel F{\"a}hndrich and
> >         Chris Hawblitzel and Orion Hodson and Steven Levi and
> >         Nick Murphy and Bjarne Steensgaard and David Tarditi and
> >         Ted Wobber and Brian D. Zill",
> >   title               = "An Overview of the {S}ingularity Project",
>
> Thank you for those interesting pointers. Interestingly both Spark
> language and Sing# language used in Singularity contains
> Design-by-Contract-like features (pre- and post-conditions, invariants,
> ...).
>
> Does anybody know if there is research on design-by-contract (as used in
> Eiffel or Spark) and type inference (as used in OCaml)? For example,
> relationships between both mechanisms, how the compiler could infer
> contracts for a sub-class of a class, how contracts can be maintained
> with minimal work from the programmer (a very useful property of ML type
> inference), how contract can be statically checked using type inference
> information, etc.
>
> Best wishes,
> d.
> --
> GPG/PGP key: A3AD7A2A David MENTRE <dmentre@linux-france.org>
> 5996 CC46 4612 9CA4 3562  D7AC 6C67 9E96 A3AD 7A2A
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>

[-- Attachment #2: Type: text/html, Size: 3518 bytes --]

Re: [Caml-list] Design-by-contract and Type inference?

[Kenn Knowles]

On Sun, Feb 04, 2007 at 04:47:48PM +0100, David MENTRE wrote:
> Does anybody know if there is research on design-by-contract (as used in
> Eiffel or Spark) and type inference (as used in OCaml)?

I happen to have recently done a little something in this area, though not in an
object-oriented setting.  Other than the citations in my related work section,
there is a presentation adjacent to mine at ESOP that does some inference in a
dependent type system (cited below).

@inproceedings{
   title = "Type Reconstruction for General Refinement Types",
   author =  "Kenneth Knowles and Cormac Flanagan",
   booktitle = "ESOP",
   year = 2007,
   url = "http://kenn.frap.net/publications/knowles-flanagan.esop.07.type.pdf"
}

@inproceedings{
   title = "Dependent Types for Low-Level Programming",
   author = "Jeremy Condit and Matthew Harren and Zachary Anderson and David Gay and George C. Necula",
   booktitle = "ESOP",
   year = "2007"
}

Hope these help,

- Kenn

Re: [Caml-list] Design-by-contract and Type inference?

[Hendrik Tews]

David MENTRE <dmentre@linux-france.org> writes:

   Does anybody know if there is research on design-by-contract (as used in
   Eiffel or Spark) and type inference (as used in OCaml)? For example,
   relationships between both mechanisms, how the compiler could infer
   contracts for a sub-class of a class, how contracts can be maintained
   with minimal work from the programmer (a very useful property of ML type
   inference), how contract can be statically checked using type inference
   information, etc.

JML for Java is similar to what Eiffel provides. There are a lot
of tools for JML, for instance ESC/Java for automatics static
checks.

Hendrik

Re: [Caml-list] Design-by-contract and Type inference?

[Oliver Bandel]

Hello,


On Tue, Feb 06, 2007 at 10:29:10AM +0100, Hendrik Tews wrote:
> David MENTRE <dmentre@linux-france.org> writes:
> 
>    Does anybody know if there is research on design-by-contract (as used in
>    Eiffel or Spark) and type inference (as used in OCaml)? For example,
>    relationships between both mechanisms, how the compiler could infer
>    contracts for a sub-class of a class, how contracts can be maintained
>    with minimal work from the programmer (a very useful property of ML type
>    inference), how contract can be statically checked using type inference
>    information, etc.


As far as I know (but I only have seen some simple examples of it),
Design by contract is a way, to make a contract between people
(or for one developer with himself/herself) so that there is an
interface, that will be agreed on.

This is only text with no effect on the code, something like
an interface-description inside comments.

(But maybe it can also be used in different ways, which I don#t know).

As far as I can see, the OCaml's module system (with module-keyword,
or mli-files) offers a contract also, but one, that also has effect
on the program, and is not only comment: editing the signature
in a   "sig ... end" or in an mli-file directly has effect
on what can be seen from the outside of that module.

And that is a contract which necessarily must be accepted.
It's more than only a comment. It's working code.

If you also use abstract types, then it's also not possible
to make awful things inside a module/compilation unit.

> 
> JML for Java is similar to what Eiffel provides. There are a lot
> of tools for JML, for instance ESC/Java for automatics static
> checks.
[...]

You can use the compiler to give you the
signature.

For example

$ ocamlc -i example.ml

Will give you the signature of your file.
But ifyou have narrowed the signature by explicitly
doing it with "sig ... end", then only the explicit
signature will be shown.

Letting the compiler show the signature of your compilation
unit can help a lot in providing *.mli files.

In the above example, it could be done with

$ ocamlc -i example.ml > example.mli

and afterwards you can edit the mli-file.

And the mli-file could be used in a team of developers
in a way that only certain people coulkd edit it, so
that nothing can become broken.
Than the interface is valid and all developers have to use it.

Ciao,
   Oliver

Re: [Caml-list] Design-by-contract and Type inference?

[Alwyn Goodloe]

In a related note I believe a student at Cambridge University
has done some work on ESC/Haskell that would support
design by contract for Haskell. This leads one to believe that
one could probably build a version of ESC for OCAML.

Alwyn


On Feb 6, 2007, at 3:45 PM, Oliver Bandel wrote:

> Hello,
>
>
> On Tue, Feb 06, 2007 at 10:29:10AM +0100, Hendrik Tews wrote:
>> David MENTRE <dmentre@linux-france.org> writes:
>>
>>    Does anybody know if there is research on design-by-contract  
>> (as used in
>>    Eiffel or Spark) and type inference (as used in OCaml)? For  
>> example,
>>    relationships between both mechanisms, how the compiler could  
>> infer
>>    contracts for a sub-class of a class, how contracts can be  
>> maintained
>>    with minimal work from the programmer (a very useful property  
>> of ML type
>>    inference), how contract can be statically checked using type  
>> inference
>>    information, etc.
>
>
> As far as I know (but I only have seen some simple examples of it),
> Design by contract is a way, to make a contract between people
> (or for one developer with himself/herself) so that there is an
> interface, that will be agreed on.
>
> This is only text with no effect on the code, something like
> an interface-description inside comments.
>
> (But maybe it can also be used in different ways, which I don#t know).
>
> As far as I can see, the OCaml's module system (with module-keyword,
> or mli-files) offers a contract also, but one, that also has effect
> on the program, and is not only comment: editing the signature
> in a   "sig ... end" or in an mli-file directly has effect
> on what can be seen from the outside of that module.
>
> And that is a contract which necessarily must be accepted.
> It's more than only a comment. It's working code.
>
> If you also use abstract types, then it's also not possible
> to make awful things inside a module/compilation unit.
>
>>
>> JML for Java is similar to what Eiffel provides. There are a lot
>> of tools for JML, for instance ESC/Java for automatics static
>> checks.
> [...]
>
> You can use the compiler to give you the
> signature.
>
> For example
>
> $ ocamlc -i example.ml
>
> Will give you the signature of your file.
> But ifyou have narrowed the signature by explicitly
> doing it with "sig ... end", then only the explicit
> signature will be shown.
>
> Letting the compiler show the signature of your compilation
> unit can help a lot in providing *.mli files.
>
> In the above example, it could be done with
>
> $ ocamlc -i example.ml > example.mli
>
> and afterwards you can edit the mli-file.
>
> And the mli-file could be used in a team of developers
> in a way that only certain people coulkd edit it, so
> that nothing can become broken.
> Than the interface is valid and all developers have to use it.
>
> Ciao,
>    Oliver
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

Re: [Caml-list] Design-by-contract and Type inference?

[Jacques Carette]

More than "some work".  I talked with her at PEPM (right before POPL), 
and ESC/Haskell is very much alive, and very cool.  Details available at
http://www.cl.cam.ac.uk/~nx200/

ESC/Ocaml for the 'functional core' should be straightforward enough 
but, as usual, the imperative features make life considerably more complex.

Jacques

Alwyn Goodloe wrote:
> In a related note I believe a student at Cambridge University
> has done some work on ESC/Haskell that would support
> design by contract for Haskell. This leads one to believe that
> one could probably build a version of ESC for OCAML.
>
> Alwyn
>
>