A Draft Specification of The CABOOSE Kernel

Team. Algebraic specification works well with abstract data types (ADTs). An ADT and an object are nearly synonymous. Since we have used an object-oriented language for creating our prototype, we will use this form of specification. An algebraic specification of a module has four sections: identification, description, operations, and axioms (rules).

The identification section has three parts: the specification name, its sort (type), and an import list describing any other specifications which it makes use of in its definition. The description section is a natural language description of the sort. The operation section list the method signatures of the accessible behavior of the module. Finally, the axioms section list any rules constraining the results of the module's methods.

Below is a draft specification for the Kernel object which provides content that the general purpose servlet returns.

---<KERNEL>--------------------------------------------------------------------------------------

sort Kernel
imports VIEW_MODEL, java.lang.String, javax.servlet.ServletContext,
javax.servlet.http.HttpServletRequest, javax.servlet.http.HttpServletResponse

--------------------------------------------------------------------------------------------------

 This is the kernel of the CABOOSE general purpose servlet. Its purpose is handling any
 incoming http request with the help of support classes.

 Implicit Contract Requirements and Guidelines: The CAB contracts with support
 classes that have rendering methods which return String content. These
 methods also must have the signature public String methodName(
 java.util.HashMap<String,String> aMapParameter ) by implicit contract. If
 they do not, the reflection activities which automatically invoke them will
 fail since they cannot find the requested method. Class, method, tile
 replacement, and stencil filename identifiers are all stored in a file called
 directory.xml which contains a mapping between each item.

---------------------------------------------------------------------------------------------------

private String gettingTheResponseStencil(javax.servlet.ServletContext theServletContext, String aStencilFileName) throws Exception

String preparingTheExceptionResponse(javax.servlet.ServletContext theServletContext,javax.servlet.http.HttpServletRequest theHTTPServletRequest,javax.servlet.http.HttpServletResponse theHTTPServletResponse)

String preparingTheSuccessfulResponse(String theViewId, javax.servlet.ServletContext theServletContext,javax.servlet.http.HttpServletRequest theHTTPServletRequest,javax.servlet.http.HttpServletResponse theHTTPServletResponse) throws Exception

private org.w3c.dom.Document gettingTheDirectoryXMLDocument(javax.servlet.ServletContext theServletContext) throws Exception

void populatingTheDirectoryMap(javax.servlet.ServletContext theServletContext) throws Exception

------------------------------------------------------------------------------------------------------

gettingTheResponseStencil(theServletContext,aStencilFileName) <> ( "" | null )

preparingTheExceptionResponse(theServletContext,theHTTPServletRequest,theHTTPServletResponse) <> ( "" | null )

preparingTheSuccesfulResponse(theServletContext,theHTTPServletRequest,theHTTPServletResponse) <> ( "" | null )

populatingTheDirectoryMap(theServletContext) <> ( .size() == 0 | null )

----------------------------------------------------------------------------------------------------------------


 The type (sort) VIEW_MODEL imported in the KERNEL specification is below:

---<VIEW_MODEL>--------------------------------------------------------------------------------------

sort ViewModel
imports java.util.HashMap, java.lang.String

----------------------------------------------------------------------------------------------------------------

 This represents a model of a single view which the controller can return

----------------------------------------------------------------------------------------------------------------

String gettingTheStencilFileName() throws Exception

java.util.HashMap<String, String> gettingTheTileRendererMappings() throws Exception

void settingTheStencilFileName(String aStencilFileName) throws Exception

void settingTheTileRendererMappings(java.util.HashMap<String, String> aSetOfTileRendererMappings) throws Exception


--------------------------------------------------------------------------------------------------------------

gettingTheStencilFileName() <> ( "" | null )

gettingTheTileRendererMappings() <> ( null )

---------------------------------------------------------------------------------------------------------------

We will be reasoning from this specification during the first product life-cycle after 02.15.2015. If you need a brief review of formal specification or an introduction see this chapter by Ian Sommerville:

http://ifs.host.cs.st-andrews.ac.uk/Books/SE9/WebChapters/PDF/Ch_27_Formal_spec.pdf

It was listed earlier in last week's posts.

Enjoy your weekend. La-La.