1.
Meyer, B.: Object-Oriented Software Construction. Prentice-Hall International, Upper Saddle River (1988)
2.
Bjørner, D., Jones, C. (eds.): The Vienna Development Method: The Meta-Language. Lecture Notes in Computer Science, vol. 61. Springer (1978)
3.
Fitzgerald, J., Larsen, P.G.: Modelling Systems—Practical Tools and Techniques in Software Development, 2nd edn. Cambridge University Press, Cambridge (2009). doi:
10.1017/CBO9780511626975
CrossRefMATH
4.
Fitzgerald, J.S., Larsen, P.G., Verhoef, M.: Vienna Development Method. Wiley Encyclopedia of Computer Science and Engineering. Wiley (2008)
5.
Woodcock, J., Davies, J.: Using Z—Specification, Refinement, and Proof. Prentice Hall International Series in Computer Science. Hertfordshire, UK (1996)
6.
Jones, C.B.: Software Development A Rigorous Approach. Prentice-Hall International, Englewood Cliffs (1980)
MATH
8.
Burdy, L., Cheon, Y., Cok, D., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. Int. J. Softw. Tools Technol. Transf.
7, 212–232 (2005)
CrossRef
9.
Larsen, P.G., Battle, N., Ferreira, M., Fitzgerald, J., Lausdahl, K., Verhoef, M.: The overture initiative integrating tools for VDM. SIGSOFT Softw. Eng. Notes
35(1), 1–6 (2010). doi:
10.1145/1668862.1668864
CrossRef
11.
Jørgensen, P.W.V., Couto, L.D., Larsen, M.: A code generation platform for VDM. In: Proceedings of the 12th Overture workshop (2014)
12.
Cok, D.: OpenJML: JML for Java 7 by Extending OpenJDK. In: Bobaru, M., Havelund, K., Holzmann, G., Joshi, R. (eds.) NASA Formal Methods. Lecture Notes in Computer Science, vol. 6617, pp. 472–479. Springer, Berlin. doi:
10.1007/978-3-642-20398-5_35(2011)
13.
Larsen, P.G., Lausdahl, K., Battle, N., Fitzgerald, J., Wolff, S., Sahara, S., Verhoef, M., Tran-Jørgensen, P.W.V., Oda, T., Chisholm, P.: The VDM-10 Language Manual. Tech. Rep. TR-2010-06, The Overture Open Source Initiative (2010)
14.
Andrews, D., Bruun, H., Damm, F., Dawes, J., Hansen, B., Larsen, P., Parkin, G., Plat, N., Totenel, H.: A Formal Definition of VDM-SL. Tech. Rep. 1998/9, Leicester University (1998)
15.
Lausdahl, K., Larsen, P.G., Battle, N.: A deterministic interpreter simulating a distributed real time system using VDM. In: Qin, S., Qiu, Z. (eds.) Proceedings of the 13th International Conference on Formal methods and Software Engineering. Lecture Notes in Computer Science, vol. 6991, pp. 179–194. Springer, Berlin. doi:
10.1007/978-3-642-24559-6_14. ISBN 978-3-642-24558-9 (2011)
16.
Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Kiniry, J.: JML Reference Manual, revision 2344 edn. (2013)
20.
Yi, J., Robby, Deng, X., Roychoudhury, A.: Past expression: encapsulating pre-states at post-conditions by means of AOP. In: Proceedings of the 12th Annual International Conference on Aspect-oriented Software Development, AOSD ’13, pp. 133–144. ACM. doi:
10.1145/2451436.2451453 (2013)
21.
McCarthy, J.: A Basis for a Mathematical Theory of Computation. In: Western Joint Computer Conference (1961)
22.
Tran-Jørgensen, P.W.V.: Automated translation of VDM-SL to JML-annotated Java. Department of Engineering, Aarhus University, Tech. rep. (2016)
23.
Larsen, P.G., Lausdahl, K., Battle, N.: Combinatorial testing for VDM. In: Proceedings of the 2010 8th IEEE International Conference on Software Engineering and Formal Methods, SEFM ’10, pp. 278–285. IEEE Computer Society, Washington, DC, USA. doi:
10.1109/SEFM.2010.32. ISBN 978-0-7695-4153-2 (2010)
24.
Tran-Jørgensen, P.W.V., Larsen, P.G., Battle, N.: Using JML-based code generation to enhance test automation for VDM models. In: Proceedings of the 14th Overture Workshop (2016)
25.
Fitzgerald, J., Larsen, P.G., Mukherjee, P., Plat, N., Verhoef, M.: Validated Designs for Object-Oriented Systems. Springer, New York (2005). doi:
10.1007/b138800
MATH
26.
Vilhena, C.: Connecting between VDM++ and JML. Master’s thesis, Minho University with exchange to Engineering College of Aarhus (2008)
27.
Jin, D., Yang, Z.: Strategies of modeling from VDM-SL to JML. In: International Conference on Advanced Language Processing and Web Information Technology, pp. 320–323 (2008)
28.
Rumbaugh, J., Jacobson, I., Booch, G.: Unified Modeling Language Reference Manual, 2nd edn. Pearson Higher Education, Boston (2004)
29.
Zhou, J., Jin, D.: Research on modeling from VDM-SL to JML for systematic software development. Control and Decision Conference (CCDC). 2010 Chinese, pp. 2312–2317. IEEE, Xuzhou (2010)
30.
Larsen, P.G.: Ten years of historical development: “Bootstrapping” VDMTools. J. Univers. Comput. Sci.
7(8), 692–709 (2001)
MATH
31.
Rivera, V., Cataño, N., Wahls, T., Rueda, C.: Code generation for event-B. Int. J. Softw. Tools Technol. Transf. 19:1–22 (2015)
32.
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)
CrossRefMATH
33.
Lensink, L., Smetsers, S., van Eekelen, M.: Generating verifiable Java code from verified PVS specifications. In: Goodloe, A., Person, S. (eds.) NASA Formal Methods. Lecture Notes in Computer Science, vol. 7226, pp. 310–325. Springer, Berlin. doi:
10.1007/978-3-642-28891-3_30 (2012)
34.
Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) 11th International Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 607, pp. 748–752. Springer, Saratoga (1992)
36.
Hubbers, E., Oostdijk, M.: Generating JML specifications from UML state diagrams. In: Forum on Specification and Design Languages FDL’03, Frankfurt, Germany, pp 263–273, September 23–26, 2003
37.
Zhen, Z.: Java Card Technology for Smart Cards. Prentice-Hall, Boston (2000)
38.
Klebanov, A.: Automata-based programming technology extension for generation of JML annotated Java card code. In: Proceedings of the Spring/Summer Young Researchers’ Colloquium on Software Engineering, pp. 41–44 (2008)
39.
Cok, D.R.: Reasoning with specifications containing method calls and model fields. J. Object Technol.
4(8), 77–103 (2005)
CrossRef
