4 ms·

E. Hehner has a course called "Formal Methods for Software Design", which he presents completely openly online (including video lectures, a textbook, solutions,

by bmer 10y ago

E. Hehner has a course called "Formal Methods for Software Design", which he presents completely openly online (including video lectures, a textbook, solutions, and so on): http://www.cs.toronto.edu/~hehner/FMSD/ http://www.cs.toronto.edu/~hehner/FMSD/ I really liked it. I also liked R. Backhouse's approach to it, encapsulated in two books: 1) less playful: http://www.amazon.com/Program-Construction-Calculating-Implementations-Specifications/dp/0470848820 http://www.amazon.com/Program-Construction-Calculating-Imple... 2) more playful: http://www.amazon.com/Algorithmic-Problem-Solving-Roland-Backhouse/dp/0470684534 http://www.amazon.com/Algorithmic-Problem-Solving-Roland-Bac... If you are looking for motivation, you might also like: http://research.microsoft.com/en-us/um/people/lamport/pubs/proof.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/p... ----------------- I found Dijkstra's stuff to be easier to read after I had read books by Hehner/Backhouse, even though chronologically, Dijkstra came first.

nickpsecurity 10y ago
Hehner's work is on my reading list. The reviews on Backhouse's links aren't promising.
- bmer 10y ago
  I have learned not to put much weight in Amazon reviews for technical literature. Borrow a copy of the books from a library (my city library actually had access to a digital version of Backhouse's latest book, and you could always Yarr! yourself a copy) and check them out, before shelling out the cash :)
  - nickpsecurity 10y ago
    Well, the one reviewer said it was only a start toward a method for practical software with practical part maxing out at a sorting algorithm. Is that true or do you have examples of realistic stuff covered by book?
    - bmer 10y ago
      Backhouse's more playful book, focuses primarily on teaching one how to write and use proofs in the "calculational style" of Dijkstra/Hoare/Lamport/others. Backhouse's less playful book covers the same topic, but has some more programming examples: * cyclic code error correction * simple sorting algorithms * real number to integer conversion is used to introduce Galois connections Again, this isn't a lot in terms of "practical examples". No production level software is built here. If you're looking for that sort of stuff, maybe you want to try out L. Lamport's book: http://www.amazon.com/Specifying-Systems-Language-Hardware-Engineers/dp/032114306X http://www.amazon.com/Specifying-Systems-Language-Hardware-E... I haven't read that book though.
      - nickpsecurity 10y ago
        Anyone that knows about all these resources should really scour them to put together a list of their application to real-world problems. Any researchers that like the stuff should apply them to real-world problems. The reason is that we don't know if such methods are a waste of time or useful until that happens. So, I'm interested in anything you have on that. EDIT: Your recommendation was good as it clearly has practical advice. I can tell just looking at table of contents. And, as a gift, I found the whole book for free plus other things in link below. :) http://research.microsoft.com/en-us/um/people/lamport/tla/book.html http://research.microsoft.com/en-us/um/people/lamport/tla/bo...
Cyph0n 10y ago
Thank you for linking that course. I've always been interested in formal methods and verification of correctness.
- bmer 10y ago
  No problem. You'll notice as you go through the links that none are about verification of correctness. Rather, they are about "correct by construction".

by bmer 10y ago

nickpsecurity 10y ago

Hehner's work is on my reading list. The reviews on Backhouse's links aren't promising.

bmer 10y ago
I have learned not to put much weight in Amazon reviews for technical literature. Borrow a copy of the books from a library (my city library actually had access to a digital version of Backhouse's latest book, and you could always Yarr! yourself a copy) and check them out, before shelling out the cash :)
- nickpsecurity 10y ago
  Well, the one reviewer said it was only a start toward a method for practical software with practical part maxing out at a sorting algorithm. Is that true or do you have examples of realistic stuff covered by book?
  - bmer 10y ago
    Backhouse's more playful book, focuses primarily on teaching one how to write and use proofs in the "calculational style" of Dijkstra/Hoare/Lamport/others. Backhouse's less playful book covers the same topic, but has some more programming examples: * cyclic code error correction * simple sorting algorithms * real number to integer conversion is used to introduce Galois connections Again, this isn't a lot in terms of "practical examples". No production level software is built here. If you're looking for that sort of stuff, maybe you want to try out L. Lamport's book: http://www.amazon.com/Specifying-Systems-Language-Hardware-Engineers/dp/032114306X http://www.amazon.com/Specifying-Systems-Language-Hardware-E... I haven't read that book though.
    - nickpsecurity 10y ago
      Anyone that knows about all these resources should really scour them to put together a list of their application to real-world problems. Any researchers that like the stuff should apply them to real-world problems. The reason is that we don't know if such methods are a waste of time or useful until that happens. So, I'm interested in anything you have on that. EDIT: Your recommendation was good as it clearly has practical advice. I can tell just looking at table of contents. And, as a gift, I found the whole book for free plus other things in link below. :) http://research.microsoft.com/en-us/um/people/lamport/tla/book.html http://research.microsoft.com/en-us/um/people/lamport/tla/bo...

Cyph0n 10y ago

Thank you for linking that course. I've always been interested in formal methods and verification of correctness.

bmer 10y ago
No problem. You'll notice as you go through the links that none are about verification of correctness. Rather, they are about "correct by construction".