Albatross – A Programming Language with Static Verification

http://albatross-lang.sourceforge.net

by helmut_brandl • 11 years ago

15 7 11 years ago

albatross-lang.sourceforge.net

mafribe3• 11 years ago

This appears to be a language in the Eiffel tradition, but with a much more expressive logic that enables full correctness proofs.

What I couldn't work out from a brief scan of the documentation is what logic is being used, and if the system is in the Curry-Howard tradition or more and LCF-style system, or something altogether different. I'm slightly worried about this since the language is imperative, and the ability fully to specify and reason about imperative languages is quite involved, e.g. you can have aliasing of memory locations.

helmut_brandl3• 11 years ago

The used logic: Classical predicate logic + Hoare Logic.

Aliasing is an issue in verifying any programming language with imperative elements and mutable data types. However this issue is addressed properly in Albatross.

mafribe3• 11 years ago

Thank you for the reply!

How are Hoare logic and predicate logic integrated? Hoare logic can be seen as a form of second-order predicate logic. What kind of Hoare logic, total correctness, partial correctness or both? There are two main approaches to dealing with aliases, separating conjunction and content quantification. Which do you use? Both become much more complex in the presence of ML-like extrudable scope, e.g.

   let x = ref 3 in 
   let f y = x++; x+y in ( f, x )

rubynl• 11 years ago

Looks very interesting! I am very curious how a non-trivial program with proof looks :)

Albatross – A Programming Language with Static Verification

Related Stories