Understanding formal specifications through good examples

ABSTRACT

Formal specifications of software applications are hard to understand, even for domain experts. Because a formal specification is abstract, reading it does not immediately convey the expected behaviour of the software. Carefully chosen examples of the software’s behaviour, on the other hand, are concrete and easy to understand—but poorly-chosen examples are more confusing than helpful. In order to understand formal specifications, software developers need good examples.

We have created a method that automatically derives a suite of good examples from a formal specification. Each example is judged by our method to illustrate one feature of the specification. The generated examples give users a good understanding of the behaviour of the software. We evaluated our method by measuring how well students understood an API when given different sets of examples; the students given our examples showed significantly better understanding.

References

1. Thomas Arts, John Hughes, Joakim Johansson, and Ulf Wiger. 2006. Testing telecoms software with quviq quickcheck. In Proceedings of the 2006 ACM SIGPLAN workshop on Erlang . ACM, 2–10.
2. Thomas Arts, John Hughes, Ulf Norell, and Hans Svensson. 2015. Testing AUTOSAR software with QuickCheck. In Software Testing, Verification and Validation Workshops (ICSTW), 2015 IEEE Eighth International Conference on . IEEE, 1–4.
3. David A Burke and Kristofer Johannisson. 2005. Translating formal software specifications to natural language. In International Conference on Logical Aspects of Computational Linguistics . Springer, 51–66.
4. Raymond P. L. Buse and Westley Weimer. 2012. Synthesizing API Usage Examples. In Proceedings of the 34th International Conference on Software Engineering (ICSE ’12) . IEEE Press, Piscataway, NJ, USA, 782–792. http://dl.acm.org/citation.cfm?id=2337223.2337316
5. Koen Claessen and John Hughes. 2011. QuickCheck: a lightweight tool for random testing of Haskell programs. Acm sigplan notices 46, 4 (2011), 53–64.
6. Jacob Cohen. 1988. Statistical Power Analysis for the Behavioral Sciences. Routledge.
7. Stefan Endrikat, Stefan Hanenberg, Romain Robbes, and Andreas Stefik. 2014. How Do API Documentation and Static Typing Affect API Usability?. In Proceedings of the 36th International Conference on Software Engineering (ICSE 2014) . ACM, New York, NY, USA, 632–642.
8. Lars Fischer and Stefan Hanenberg. 2015. An Empirical Investigation of the Effects of Type Systems and Code Completion on API Usability Using TypeScript and JavaScript in MS Visual Studio. In Proceedings of the 11th Symposium on Dynamic Languages (DLS 2015) . ACM, New York, NY, USA, 154–167.
9. Alex Gerdes, John Hughes, Nick Smallbone, and Meng Wang. 2015. Linking Unit Tests and Properties. In Proceedings of the 14th ACM SIGPLAN Workshop on Erlang (Erlang 2015) . ACM, New York, NY, USA, 19–26.
10. J. Hofmeister, J. Siegmund, and D. V. Holt. 2017. Shorter identifier names take longer to comprehend. In 2017 IEEE 24th International Conference on Software Analysis, Evolution and Reengineering (SANER) . 217–227.
11. John Hughes. 2016. Experiences with QuickCheck: testing the hard stuff and staying sane. In A List of Successes That Can Change the World . Springer, 169–186.
12. Jinhan Kim, Sanghoon Lee, Seung-won Hwang, and Sunghun Kim. 2009. Adding examples into Java documents. In Automated Software Engineering, 2009. ASE’09. 24th IEEE/ACM International Conference on . IEEE, 540–544.
13. Sebastian Kleinschmager, Stefan Hanenberg, Romain Robbes, Éric Tanter, and Andreas Stefik. 2012. Do static type systems improve the maintainability of software systems? An empirical study. In IEEE 20th International Conference on Program Comprehension, ICPC 2012, Passau, Germany, June 11-13, 2012 . 153–162.
14. Benoit Lavoie, Owen Rambow, and Ehud Reiter. 1996. The ModelExplainer. In Proceedings of the 8th international workshop on natural language generation . 9–12.
15. Dawn Lawrie, Christopher Morrell, Henry Feild, and David Binkley. 2006. What’s in a Name? A Study of Identifiers. In Proceedings of the 14th IEEE International Conference on Program Comprehension (ICPC ’06) . IEEE Computer Society, Washington, DC, USA, 3–12.
16. Lee Wei Mar, Ye-Chi Wu, and Hewijin Christine Jiau. 2011. Recommending proper API code examples for documentation purpose. In Software Engineering Conference (APSEC), 2011 18th Asia Pacific . IEEE, 331–338.
17. Vibhu O Mittal and Cécile Paris. 1994. Generating examples for use in tutorial explanations: using a subsumption based classifier. In Proceedings of the 11th European Conference on Artificial Intelligence . John Wiley & Sons, Inc., 530–534.
18. João Eduardo Montandon, Hudson Borges, Daniel Felix, and Marco Tulio Valente. 2013. Documenting APIs with examples: Lessons learned with the APIMiner platform. In Reverse Engineering (WCRE), 2013 20th Working Conference on . IEEE, 401–408.
19. Laura Moreno, Gabriele Bavota, Massimiliano Di Penta, Rocco Oliveto, and Andrian Marcus. 2015. How Can I Use This Method?. In Proceedings of the 37th International Conference on Software Engineering - Volume 1 (ICSE ’15) . IEEE Press, Piscataway, NJ, USA, 880–890. http://dl.acm.org/citation.cfm?id=2818754.2818860
20. William R Swartout. 1982. GIST English Generator.. In AAAI. 404–409.
21. Phillip Merlin Uesbeck, Andreas Stefik, Stefan Hanenberg, Jan Pedersen, and Patrick Daleiden. 2016. An Empirical Study on the Impact of C++ Lambdas and Programmer Experience. In Proceedings of the 38th International Conference on Software Engineering (ICSE ’16) . ACM, New York, NY, USA, 760–771.
22. Claes Wohlin, Per Runeson, Martin Höst, Magnus C. Ohlsson, and Björn Regnell. 2012. Experimentation in Software Engineering. Springer.

Index Terms

• Software and its engineering

  • Software creation and management

    • Software verification and validation

      • Software defect analysis

  • Software notations and tools

    • Context specific languages

      • Programming by example