TryOpenJML - A Verily based web application for learning about the Java Modeling Language

This thesis has a two-fold purpose. On the one hand, the web applications are an important part of life. On a day to day basis, from managing our heath care choices to banking, to connecting to a friend, almost everything is done through a web application. Development of these applications is also a very trend-driven domain. Numerous web frameworks are available today, but almost none has been created taking reliability into consideration. With the combination of application construction recipes and static analysis, the Verily framework was created to build more reliable web applications. On the other hand, the goal of the Java Modeling Language (JML) has to be conveyed to the world. It is a language that can go hand in hand with existing code, having a wide range of tools that help build practical and effective designs. There are many tools available for JML: jmldoc for web pages, jmlunit for unit tests, jmlc for class files, etc. I will be using the tools for Runtime Assertion Checking (RAC) and Extended Static Checking (ESC). These checks warn about the possible runtime exceptions and assertion violations. The benefits of JML assert statements over Java assertions are that they support all JML features. The question that I am concerned with, in this thesis, is how the Verily Framework can contribute to the domain of web application development. Keeping this question in mind, my objective is to create a tutorial which will aid in learning about JML. The tutorial will let the potential users read and write JML specifications and use JML tools, explain basic JML semantics, and let them know where to go for help if they need more details