Typestates for Objects R. DeLine and M. Fähnrich In Proceedings of the European Conference on Object-oriented Programming (ECOOP '04), June 2004.Slide 2Main ContributionsMain Contributions (continued)Problem StatementResource ProtocolsState-machine protocolsSlide 8Typestates for ObjectsExampleSupport for ModularityNotation for TypestatesSpecial IssuesCompositionObject Typestate RevisitedDowncasting, Upcasting, etc…Typestates and Subclassing -1Typestates and Subclassing - 2Typestates and Subclassing - 3There is a problemCorrected WebPageFetcherSliding methodsSliding Method: Case 1Sliding Method: Case 2Non-virtual call siteSlide 26Virtual call siteSlide 28Extensibility through SubclassingAliasing[NotAliased] Parameter[NotAliased] FieldLeakingFormal ModelAvailable ImplementationLimitations with ApproachSlide 37Additional Content: Custom StatesIEnumerator ExampleDiscussionEditorial OpinionTypestates for ObjectsR. DeLine and M. FähnrichIn Proceedings of the European Conference on Object-oriented Programming (ECOOP '04), June 2004.Presented byMarwan Abi-AntounCS 15-819: Objects and Aspects: Language Support for Extensible and Evolvable SoftwareFall 2004Main Contributions•Extension to notion of conventional type:–Type: set of operations ever permitted on an object–Typestate: subset of operations on an object permitted in a particular context or a particular calling sequence•A programming model:–Detect at compile time using static analysis, nonsensical execution sequences–Such defects not detected by type checking or static scoping rulesMain Contributions (continued)•Novel Object-Oriented support:–Supports modern object-oriented languages–Composition–Sub-classing (downcast, upcast, etc…)•Performs alias detection and confinement•Supports extensibility and modularity•Implementation available Microsoft .NET platformProblem Statement•Interfaces have usage rules or protocols•Typically mentioned in documentation•Documentation not useful for checking•Interface rules fall into broad categories:–Resource Protocols–State Machine Protocols–“Calling conventions”•Parameter or return value cannot be nullResource Protocols•A resource is an object meant to be released through an explicit method call rather than through garbage collection (e.g., a file handle)•Resource Guarantee: –No resource is referenced after its release–All resources are released or returned to the method’s callerState-machine protocols•Limit the order in which an object’s methods can be called to the transitions of a finite state machine–States have arbitrary symbolic names–Transitions between states labeled with method names•Method Order Guarantee: –String of method calls made on an instance of that class must be in language accepted by finite state machineTypestates for Objects•Generalization of original notion1 of typestate to an abstract named predicate over object graphs•An object is in different typestates over its lifetime•Typestate changes when the object’s state (including any nested objects) changes•Remark: Not to be confused with invariants •Invariant remains true over the object’s lifetime, i.e., an invariant holds in all typestates1. Typestate: A Programming Language Concept for Enhancing Software Reliability, by Robert E. Strom and Shaula Yemini, 1986ExampleRestrict return valueRestrict parameterMethod post-conditionMethod pre-conditionWebPageFetcher typestateField object typestateSocket typestatePredicates over object graphs: recursive typestate about state of referenced objectsNo aliasingInvariant (holds in all typestates)Support for Modularity•Client view:–Predicate uninterpreted function to be matched by name–Analysis inspects callee’s declaration and not its body•Implementor view:–Predicate defined in terms of predicates over the fields valuesClient view of state machine for WebPageFetcherImplementor view of state machine for WebPageFetcher•Mechanically verify state machine protocol:–Pre-condition: symbolic state the object must be in to call a method; –Post-condition is a symbolic state the object is in after the method returnsNotation for Typestates•Typestate specification applies to class frame first introducing the typestate name (via TypeStates(…) annotation)•Without the annotation, objects are assumed to be in state State.Default–System.Object @ State.Default•Can be targeted at a particular class frame C–using TypeStates(…, Type = C )•Can be targeted at all subclasses –using TypeStates(…, Type = Subclasses )Special Issues•Composition–Addressed with [WhenEnclosingState]•Subclassing–Downcasting, upcasting, virtual dispatch, direct calls–Addressed with sliding method signatures•Null References–Addressed with [Null], [NotNull]•Alias detection –Addressed with [NotAliased], [MaybeAliased]Composition•Used when both the object and its fields (referencing nested objects) have state-machine protocols•State mapping–Relates state of an object to the state of its fields:–Using [WhenEnclosingState] construct•Ensures the “outer” object is well-behaved client of any nested “inner” objects with their own state machine protocolsObject Typestate Revisited•Class frame: set of fields of the object declared in that particular class, not in any super- or sub-classes.•Frame typestate: constraints on fields in a class frame•Object typestate = collection of frame typestates–one per class frame of the object’s allocated dynamic type. –rest typestate (uniform typestate for all unknown subclass frames)Downcasting, Upcasting, etc…•Downcasting: casting a pointer or reference to a base class, to a derived class.–WebPageFetcher w = new CachingFetcher ();CachingFetcher f = (CachingFetcher )w;•Upcast: casting a pointer or reference to a derived class to a more general base classCachingFetcher f = new CachingFetcher();WebPageFetcher w = (WebPageFetcher)f;•Virtual call: a call subject to dynamic dispatchTypestates and Subclassing -1A subclass can associate its own field invariants with its superclasses’ typestatesTypestates and Subclassing - 2Overriding methods can take advantage of object typestate precondition on the receiverTypestates and Subclassing - 3Typestate targeted at a particular class frameSubclass can define its own typestatesThere is a problem•Post specification states that all frames, including subclasses, will be in typestate Open at the