Apologies for commenting on the form rather than content here, but is wikia.com really the place this community decided to organize around? Seeing TV shows and cosmetic products for teenagers advertised next to an article on formal methods is… a strange experience.
That’s strange but submission has many links. Mostly a positive. The only negative I had, which is dependent on my goal of industrial adoption, is that Z notation proved too hard to understand in a lot of projects for a lot of programmers. Alternatives, many coming later, also had a better story in automatic verification of code against the specs, generation of code from specs, prover integration, and so on. It’s still interesting for people studying various kinds of logic or historical use of formal methods. I keep Z papers in my collection just in case their work ever has ideas for solving a new problem.
I wasn’t exactly sure of the best link to post here. There’s a whole book that’s available online, but I thought a portal-type link might be a better entry point.
The main one these days is Alloy. Jackson designed it specifically to address two problems he had with Z, which were that it was too intimidating to beginners and that a lot of valid Z specs couldn’t be model-checked.
It largely failed due to its learning curve. B method did, too. Both did improve software quality, though. I had a resource diving into the various methods in a detailed comparison whose criteria I want everyone doing model-checking or formal verification to consider and weight in on. Turns out I didn’t submit it even though I thought I did. Oops…
I’ve been referencing the results in comments here: Abstract, State Machines and TLA+/PlusCal came out easiest to use with high cost-benefit analysis. ASM’s and PlusCal can look pretty similar to each other and FSM’s. TLA+ even has similar foundations of Z minus the complexity. If you like Z, you might also like the concept of TLZ where Lamport combined Z with temporal logic. That link has him saying the Z and CSP community ignoring his TLZ work twice. So, he ditched Z and created something better: TLA+. It’s going mainstream with non-mathematicians picking it up thanks to the work by folks like hwayne.
Since I didn’t submit that survey and it’s late, I’ll submit it in the morning around 10-11am as usual. That way people can check it out at lunch time. Stay tuned. :)
Apologies for commenting on the form rather than content here, but is wikia.com really the place this community decided to organize around? Seeing TV shows and cosmetic products for teenagers advertised next to an article on formal methods is… a strange experience.
That’s strange but submission has many links. Mostly a positive. The only negative I had, which is dependent on my goal of industrial adoption, is that Z notation proved too hard to understand in a lot of projects for a lot of programmers. Alternatives, many coming later, also had a better story in automatic verification of code against the specs, generation of code from specs, prover integration, and so on. It’s still interesting for people studying various kinds of logic or historical use of formal methods. I keep Z papers in my collection just in case their work ever has ideas for solving a new problem.
I wasn’t exactly sure of the best link to post here. There’s a whole book that’s available online, but I thought a portal-type link might be a better entry point.
The Way of Z: https://staff.washington.edu/jon/z-book/
@nickpsecurity, what of Z’s successors would you say did a better job with being understandable to humans?
The main one these days is Alloy. Jackson designed it specifically to address two problems he had with Z, which were that it was too intimidating to beginners and that a lot of valid Z specs couldn’t be model-checked.
Survey is here.
It largely failed due to its learning curve. B method did, too. Both did improve software quality, though. I had a resource diving into the various methods in a detailed comparison whose criteria I want everyone doing model-checking or formal verification to consider and weight in on. Turns out I didn’t submit it even though I thought I did. Oops…
I’ve been referencing the results in comments here: Abstract, State Machines and TLA+/PlusCal came out easiest to use with high cost-benefit analysis. ASM’s and PlusCal can look pretty similar to each other and FSM’s. TLA+ even has similar foundations of Z minus the complexity. If you like Z, you might also like the concept of TLZ where Lamport combined Z with temporal logic. That link has him saying the Z and CSP community ignoring his TLZ work twice. So, he ditched Z and created something better: TLA+. It’s going mainstream with non-mathematicians picking it up thanks to the work by folks like hwayne.
Since I didn’t submit that survey and it’s late, I’ll submit it in the morning around 10-11am as usual. That way people can check it out at lunch time. Stay tuned. :)