A Hoare logic for call-by-value functional programs

“Computational functions are reflected, at the logical level, as pairs of a precondition and postcondition. […] A function’s precondition and postcondition alone determine how it is lifted: its code is ignored. (The conformance of a function’s body to its declared pre- and postcondition
is checked, of course, via a proof obligation […]) This reflects a philosophy in which the only way of reasoning about the behavior of a function value is via its specification: code never appears within formulae.” — It seems that it took a very long time until this extremely natural idea was finally incorporated in a decent Hoare logic for functional programs (and a couple more years until it finally reached the world of refinement type systems 😉 )

“In this paper, we […] allow specifications to be expressed in higher-order logic. The intuitive justification for this approach is that, if functions can abstract over functions, then specifications must abstract over specifications.”

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: