Concurrency : DATATYPE WITH SUBTYPES concurrent, guarded, failure %, sequential BEGIN IMPORTING java %sequentual(desc:string): sequential? : sequential %Sequential is just concurrent 1 concurrent(bound:nat, desc:string): concurrent? : concurrent guarded_lock(lock:string, desc:string): guarded_lock? : guarded guarded_bound(bound:nat, desc:string): guarded_bound? : guarded failure(bound:nat, exception:classes, desc:string): failure? : failure END Concurrency concurrency : THEORY BEGIN IMPORTING Concurrency guarded_lock: TYPE = (guarded_lock?) guarded_bound: TYPE = (guarded_bound?) END concurrency semantic_property [T:TYPE] : THEORY BEGIN IMPORTING java, jml %SemanticProperty: TYPE %get_prop: [SemanticProperty -> T] props_of_class: [classes -> set[T]] props_of_field: [fields -> set[T]] props_of_method: [methods -> set[T]] props_of_interface: [interfaces -> set[T]] END semantic_property subtype_set[T:TYPE, U: TYPE FROM T] : THEORY BEGIN S: VAR set[T] subtype_set(S): set[U] = { s:U | S(s) } % x: set[U FROM T] END subtype_set java_additions : THEORY BEGIN IMPORTING java_semantics, object c1,c2: VAR classes inherit_from(c1)(c2): bool = inherit_from(c1,c2) END java_additions max_nat: THEORY BEGIN x, y: VAR nat maximum?(x): bool = (FORALL y: y <= x) infinity: (maximum?) END max_nat set_stuff [T: TYPE]: THEORY BEGIN IMPORTING sets[T] p: VAR PRED[T] S: VAR set[T] t: VAR T none(p)(S): bool = FORALL (s:(S)): NOT(p(s)) none_is_not_some: LEMMA none(p)(S) IFF NOT(some(p)(S)) none_is_not_exists: LEMMA none(p)(S) IFF NOT(EXISTS (x:(S)): p(x)) END set_stuff defaults : THEORY BEGIN IMPORTING concurrency, max_nat DefaultConcurrent: set[concurrent] = singleton(concurrent(infinity, "")) DefaultGuardedLock: set[guarded_lock] = emptyset DefaultGuardedBound: set[guarded_bound] = emptyset DefaultFailure: set[failure] = emptyset DefaultConcurrency: set[Concurrency] = union[Concurrency](DefaultConcurrent, union[Concurrency](DefaultGuardedLock, union[Concurrency](DefaultGuardedBound, DefaultFailure))) END defaults object : THEORY BEGIN IMPORTING java_semantics, defaults, semantic_property[Concurrency] c: VAR classes Object: classes object_is_top_type: AXIOM (FORALL c: c=Object OR inherit_from(c,Object)) object_methods_all_default: AXIOM (FORALL (m:(methods(Object))): props_of_method(m) = DefaultConcurrency) END object jmlc : THEORY BEGIN IMPORTING concurrency, semantic_property[Concurrency], java_semantics, java_additions s: VAR set[Concurrency] m: VAR methods c,c1,c2: VAR classes %Helper extraction functions guarded_bounds(s): set[guarded_bound] = { p:(guarded_bound?) | s(p) } guarded_bounds(m): set[guarded_bound] = guarded_bounds(props_of_method(m)) guarded_bounds(c): set[guarded_bound] = guarded_bounds(props_of_class(c)) guarded_locks(s): set[guarded_lock] = { p:(guarded_lock?) | s(p) } guarded_locks(m): set[guarded_lock] = guarded_locks(props_of_method(m)) guarded_locks(c): set[guarded_lock] = guarded_locks(props_of_class(c)) concurrent(s): set[concurrent] = { p:concurrent | s(p) } concurrent(m): set[concurrent] = concurrent(props_of_method(m)) concurrent(c): set[concurrent] = concurrent(props_of_class(c)) failure(s): set[failure] = { p:failure | s(p) } failure(m): set[failure] = failure(props_of_method(m)) failure(c): set[failure] = failure(props_of_class(c)) locks_for_method(m): set[string] = { s:string | (EXISTS (l:(guarded_locks(m))): lock(l)=s) } locks_for_class(c): set[string] = { s:string | (EXISTS (l:(guarded_locks(c))): lock(l)=s) } parent_method_im_overriding: [methods -> lift[methods]] %TODO move out of jmlc no_parent_method_im_overriding?(m): bool = bottom?(parent_method_im_overriding(m)) top_class?(c): bool = c=Object overridden_method_properties(m): set[Concurrency] = CASES parent_method_im_overriding(m) OF bottom: emptyset, up(parent_method): props_of_method(parent_method) ENDCASES implemented_interface_methods_im_implementing: [methods -> set[methods]] overridden_and_implemented_methods(m): set[methods] = LET interface_methods:set[methods]=implemented_interface_methods_im_implementing(m) IN CASES parent_method_im_overriding(m) OF bottom: interface_methods, up(parent_method): union(interface_methods, parent_method) ENDCASES %TODO validity of some collection of java structures, not universal validity! child_gbs, parent_gbs: VAR set[guarded_bound] valid_guarded_bound_inheritance(child_gbs, parent_gbs): bool = (empty?(child_gbs) AND empty?(parent_gbs)) OR (singleton?(child_gbs) AND singleton?(parent_gbs) AND bound(parent_gbs) <= bound(child_gbs)) %For every method, either there is no guarded bound or there is one guarded bound. %If there is a guarded bound, and this method overrides a parent method, then that %parent method must have a guarded bound less than or equal to this bound. valid_method_guarded(m): bool = no_parent_method_im_overriding?(m) OR FORALL (pm:(overridden_and_implemented_methods(m))): valid_guarded_bound_inheritance(guarded_bounds(m), guarded_bounds(pm)) valid_class_guarded(c): bool = top_class?(c) OR (FORALL (p:(inherit_from(c))): valid_guarded_bound_inheritance(guarded_bounds(c), guarded_bounds(p))) %Every method must require the same locks as the parent method it overrides (if it does override). valid_method_locks(m): bool = no_parent_method_im_overriding?(m) OR FORALL (pm:(overridden_and_implemented_methods(m))): locks_for_method(m)=locks_for_method(pm) valid_class_locks(c): bool = top_class?(c) OR (FORALL (p:(inherit_from(c))): locks_for_class(c) = locks_for_class(p) ) child_cs, parent_cs: VAR set[concurrent] valid_concurrent_inheritance(child_cs, parent_cs): bool = (empty?(child_cs) AND empty?(parent_cs)) OR (singleton?(child_cs) AND singleton?(parent_cs) AND bound(parent_cs) <= bound(child_cs)) %For every method, either there is no concurrency bound or there is one concurrency bound. %If there is a concurrency bound, and this method overrides a parent method, then that %parent method must have a concurrency bound less than or equal to this bound. valid_method_concurrent(m): bool = no_parent_method_im_overriding?(m) OR valid_concurrent_inheritance(concurrent(m), concurrent(overridden_method_properties(m))) valid_class_concurrency?(c): bool = top_class?(c) OR (FORALL (p:(inherit_from(c))): valid_concurrent_inheritance(concurrent(c), concurrent(p))) %FAILURE %Each child and class has at most one failure property. %In the prescence of inheritance either the method/class has no %failure clause and the parent child_fs, parent_fs: VAR set[failure] valid_failure_inheritance?(child_fs, parent_fs): bool = (empty?(child_fs) AND empty?(parent_fs)) OR ( singleton?(child_fs) AND singleton?(parent_fs) AND bound(child_fs) = bound(parent_fs) AND inherit_from(exception(child_fs), exception(parent_fs))) valid_method_failure(m): bool = no_parent_method_im_overriding?(m) OR valid_failure_inheritance?(failure(m), failure(overridden_method_properties(m))) valid_class_failure?(c): bool = top_class?(c) OR (FORALL (p:(inherit_from(c))): valid_failure_inheritance?(failure(c), failure(p))) %TODO need a supertype of classes and interfaces that has methods defined on %valid class w.r.t. method (all method props must be identical). valid_method_class: bool = (FORALL c: (FORALL (m:(methods(c))): props_of_method(m)=props_of_class(c))) END jmlc