tag:blogger.com,1999:blog-4097792925045582567.post1604282558195351025..comments2024-02-18T15:55:05.075-05:00Comments on Reflections on Software Engineering: Thoughts on Formal Methods in Software EngineeringMichaelhttp://www.blogger.com/profile/02649257003202319541noreply@blogger.comBlogger2125tag:blogger.com,1999:blog-4097792925045582567.post-1747787888446386972013-01-03T22:23:31.644-05:002013-01-03T22:23:31.644-05:00Mike, thanks for your comment, it's great to h...Mike, thanks for your comment, it's great to hear from you! I'll look into updating the image to have the correct schema name, though regardless, I think my point is still pretty clear — Z notation, and other formal models like it, is difficult to read and, in some ways moot since mapping functions from model to code are still a major weakness.<br /><br />Also, after some serious reflection on this subject and a little growth, I changed my mind on some of these points: http://neverletdown.net/2009/12/the-domestication-of-formal-methods/. Two things brought me around from thinking formal methods were complete waste to believing that they can provide serious value in the right circumstances.<br /><br />One is seeing the WSDL 2.0 Z specification — the only "real world" Z specifications that I have ever seen. http://www.w3.org/TR/wsdl20/wsdl20-z.html The only downside to this is that I don’t think the specification was really used for anything other than… making a specification. In the context of the WSDL 2.0, that is OK, but my argument about a lack of solid mapping functions still stands. I want to see working code in the end and arguments about preventing defect injection fall apart in my opinion simply because for the cost required to create a formal mathematical model I likely could have written a piece of the system and tested it. Now, switching to a "domesticated" formal method and getting closer to the code is a really good compromise and starts to make a lot of sense in my opinion.<br /><br />The other is reading Anthony Hall’s "7 Myths of Formal Methods" paper. Mike, you are 100% correct about your second statement (and I was wrong to omit this from my essay, though at the time I didn't understand or believe it) – the model is good, but the prose that goes with the model is invaluable. Further, the process of creating the prose and model, in the right situations, is priceless. The WSDL specification is a much better example for all of these positive attributes than the toy "Birthday Book" example.Michaelhttps://www.blogger.com/profile/02649257003202319541noreply@blogger.comtag:blogger.com,1999:blog-4097792925045582567.post-89579671718062606872013-01-03T22:21:26.998-05:002013-01-03T22:21:26.998-05:00Your argument would be stronger if you had copied ...Your argument would be stronger if you had copied out those two schemas correctly, but you have given the second one the wrong name.<br /><br />And it would be fairer if you pointed out that Z specifications are usually strong on informal commentary that explains the mathematics and relates it to an informal understanding of the system being described.Mike Spiveynoreply@blogger.com