3 ms·
What would a coarse-granular specification for Excel look like? How would you prove correctness against such a spec? Examples, please. In these discussions, I o
by adwn 6y ago
What would a coarse-granular specification for Excel look like? How would you prove correctness against such a spec? Examples, please. In these discussions, I only ever see vague statements and handwaving by formal verification proponents — which is kind of ironic, when you think about it...
- rramadass 6y agoI believe you are being facetious here. This is a forum for stimulating discussions and exchange of ideas. The fact that you only "see vague statements and handwaving" is more a reflection of one's knowledge bank (or lack thereof) than any shortcoming of the subject or its proponents. By definition this is a complicated and difficult subject and when a computer science pioneer and great like Edsger Dijkstra says something, you pay attention and think about it :-) PS: "Excel" can be thought of as a program generator which specifies a metalanguage (i.e. a "grammar") for a set of DSLs (i.e. Spreadsheet formulas). A little Googling brought up "ViTSL/Gencel"(https://web.engr.oregonstate.edu/~erwig/Gencel/ https://web.engr.oregonstate.edu/~erwig/Gencel/) and "Classheets"(http://www.jot.fm/issues/issue_2007_10/paper19/index.html http://www.jot.fm/issues/issue_2007_10/paper19/index.html) showing approaches to specifying "correct" Spreadsheets.