An Axiomatic Basis for Computer Programming (1969) [pdf]

http://www.cs.toronto.edu/~chechik/courses05/csc410/readings/hoare_axiomatic.pdf

by tjalfi • 5 years ago

29 16 5 years ago

cs.toronto.edu

BruceEel• 5 years ago

A gem of readability and clarity.

cjohansson• 5 years ago

How does one read it? I simply can't read it, only see the first page

d_tr• 5 years ago

Did you try more than one viewer? It renders fine in Evince and in Vivaldi here. The 'bodies' of the pages are not regular text but images over that background gradient, by the way.

baxrob• 5 years ago

Works for me but found this less unusual pdf: http://www.cs.toronto.edu/~chechik/courses05/csc410/readings...

jasperry• 5 years ago

Thanks for posting this--I'm getting back into studying the formal semantics of programming languages. Questions for those working in this area:

According to Pierce's Types and Programming Languages, axiomatic semantics of the type that Hoare pioneered are not found as useful today as operational semantics. Is that (still) true?

Are the major approaches (operational, denotational, axiomatic) pretty much solidified now, or are there significant new efforts at finding better overall formalizing frameworks?

auggierose2• 5 years ago

There is only one formalising framework, it is called math. The rest is just noise.

When trying to make a better framework for formalising computer programs, just make a better framework for formalising math first.

Joker_vD3• 5 years ago

You can't make a better framework for formalising math, because, as you've yourself said, "there is only one formalising framework", and it's math itself. Cue the problems with self-application and Goedel's tricks :)

taeric• 5 years ago

Math has many formalisms. Some more useful than others, in certain contexts. All restricted by the norms of communication that they are written in.

So, yes, there are some math formalities for processes. No, they probably don't help in finding new processes as much as you'd think. Despite being quite good at understanding existing processes through formal exploration.

Joker_vD3• 5 years ago

Right, the axiomatic semantics aka "the Floyd-Hoare rules". The interesting thing about them is that I've read many presentations of them and not a single one of those had any mention of subroutines (procedures or functions, doesn't matter) at all. All you have is global variables, assignments, sequencing, conditions, and loops. That's it. And while one would think that adding support for subroutines would be tremendously useful, allowing for e.g. specifying correctness of data structures' implementations, apparently it has not been done.

The closest thing to it I've seen is TLA+ but holy fatcats is it unwieldy.

rssoconnor• 5 years ago

VerifiableC[1] provides Hoare rules for (a large subset[2] of) C that include function calls, pointers and heap allocation, and some amount of concurrency. It does use an extension to Hoare logic, called separation logic, to achieve some of these features. In particular, separation logic's frame rule is instrumental for the modularization needed for semantics of function calls.

[1]https://vst.cs.princeton.edu/veric/

[2]excludes setjmp/longjmp, unstructured switch statements, goto and maybe a few other moderately exotic constructions.

rramadass2• 5 years ago

https://softwarefoundations.cis.upenn.edu/

dang• 5 years ago

Hoare's thoughts on the 40th anniversary: https://cacm.acm.org/magazines/2009/10/42360-retrospective-a...

Discussed (barely) at the time:

Retrospective: An Axiomatic Basis for Computer Programming - https://news.ycombinator.com/item?id=905176 - Oct 2009 (1 comment)

rramadass2• 5 years ago

Also read Robert Floyd's paper Assigning Meanings to Programs.

After getting the gist of the above, reading Bertrand Meyer's Design by Contract and Applying Design by Contract will clarify on how to apply the ideas to "real" systems.

An Axiomatic Basis for Computer Programming (1969) [pdf]

Related Stories