Albatross – A Programming Language with Static Verification(albatross-lang.sourceforge.net)
albatross-lang.sourceforge.net
Albatross – A Programming Language with Static Verification
http://albatross-lang.sourceforge.net
3 comments
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.
Aliasing is an issue in verifying any programming language with imperative elements and mutable data types. However this issue is addressed properly in Albatross.
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.
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 )Predicate logic is the base. Hoare logic rests on top of it to reason about the effect of commands in imperative code.
Total correctness is used for Hoare logic. I.e. {Q} S {R} means that the program fragment S started in a state that satisfies Q will end up in finite steps in a state satisfying R.
For aliases I use something similar to separation logic. But I claim that it is much easier to use because it doesn't require to reason about the state of the heap. Some basic ideas can be found at https://softwareverificaton.wordpress.com/2012/06/03/abstrac.... My current concept is much more refined and not yet published.
Total correctness is used for Hoare logic. I.e. {Q} S {R} means that the program fragment S started in a state that satisfies Q will end up in finite steps in a state satisfying R.
For aliases I use something similar to separation logic. But I claim that it is much easier to use because it doesn't require to reason about the state of the heap. Some basic ideas can be found at https://softwareverificaton.wordpress.com/2012/06/03/abstrac.... My current concept is much more refined and not yet published.
If you use Hoare triples for total correctness, you can't reason about non-terminating programs. I recommend to use a Hoare logic for "generalised" correctness that enables you to reason about both, terminating and nonterminating programs.
I would be interested in your ideas about aliasing. I don't think you can avoid the complications of separation logic or content quantification.
I would be interested in your ideas about aliasing. I don't think you can avoid the complications of separation logic or content quantification.
For non-terminating programs I use processes as described by Tony Hoare in "Communicating Sequential Processes". Procedures must always terminate in Albatross.
If I have more documentation on aliasing, I can give you hint. Could you provide me some email address?
If I have more documentation on aliasing, I can give you hint. Could you provide me some email address?
Looks very interesting! I am very curious how a non-trivial program with proof looks :)
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.