Kinding with Semantic Properties
Semantic properties are used in kinding an instance (e.g., a method, a class, a type) in the following fashion. We do not have the space to fully detail the related theory and algorithm, but a detailed example should suffice is getting the idea across2. We’ll focus exclusively on kinding the above Java method to this end. It should be noted, as discussed in detail in the aforementioned thesis, that most of the below specifications are automatically generated from source assets by domain specific parsers. The basic structure of a program, its annotations, the structure and kind semantics of the programming language in which it is written, etc. are all provided for automatically. Thus, the verbosity of these specification examples should not deter the reader as nearly all of this detail is completely hidden from a typical user. The kind of this method contains much more information than its type. First, the kind contains everything we have already discussed with respect to the method’s signature. Additionally, a semantic interpretation of all of the documentation attached to the method is included. And, as a final element, a more complete representation of its type is also incorporated. In more detail: 1. All the information that is inherent in the explicit specification of the method’s signature and type are first composed. We will call this particular instance Debug.isOff. With respect to classification, this construct is a Java method. This is encoded as Debug.isOff: JAVAMETHOD We interpret the method’s signature as follows: Debug.isOff.ParameterSet _p Debug.isOff Debug.isOff.ReturnType _p Debug.isOff where Debug.isOff.ParameterSet: JAVAPARAMETERSET Debug.isOff.Parameter0 _p Debug.isOff.ParameterSet Debug.isOff.Parameter0: JAVAPARAMETER Debug.isOff.Parameter0Type _p Debug.isOff.Parameter0 Debug.isOff.Parameter0Name _p Debug.isOff.Parameter0 Debug.isOff.Parameter0Type: JAVATYPE Debug.isOff.Parameter0Type _ java.lang.Thread Debug.isOff.Parameter0Name: JAVAIDENTIFIER Debug.isOff.Parameter0Name _ thread ... etc... Effectively, we reflectively encode all of the type and signature information for the method in a kind theoretic context. The structure of the related kinds like JAVAPARAMETER encode the necessary structure that must be provided by the interpretation, a type and a name in this case. Thus, this part of the process is no different than the parsing and typing that goes along with compiling the method. 2. All the supplementary information embedded via the use of the semantic properties and extra-type information is also interpreted into a kind theoretic context. 2 The interested reader can read [18] at their leisure. For example, the fact that the method is declared as having GUARDED concurrency semantics is encoded with the concurrent kind: ConcurrencySemantics0 _p Debug.isOff ConcurrencySemantics0: JAVACONCURRENCYSEMANTICS ConcurrencySemantics0 _ GuardedSemantics Likewise, the method’s visibility, signature concurrency (use of the synchronized keyword), sideeffects (modifies), precondition, parameter and return value documentation, and meta-information (review) are also interpreted. 3. Finally, we interpret a more complete representation of the method’s type by taking advantage of the domain semantics of refinement. In this example, we attach stronger refinement semantics via the use of the specified, explicit, classical contract. The existence of the precondition means that, after we interpret such, we can: (a) Check that overridden methods properly weaken the precondition for behavioral subsumption. (b) Interpret such specification into run-time test code—here that entails just a literal insertion of the code snippet into the proper place(s) in a rewritten version of the method. (c) Use this behavioral specification as a guard in semantic composition (see below). The kind of this method is our formal “best-effort” at the specification of its semantics. Now, the rules of kind and instance composition come into play with respect to defining semantic compatibility.
|
