Global InformationTypestate analysis information
Typestate analysis, sometimes called protocol analysis, is a form of program analysis employed in programming languages. It is most commonly applied to object-oriented languages. Typestates define valid sequences of operations that can be performed upon an instance of a given type. Typestates, as the name suggests, associate state information with variables of that type. This state information is used to determine at compile-time which operations are valid to be invoked upon an instance of the type. Operations performed on an object that would usually only be executed at run-time are performed upon the type state information which is modified to be compatible with the new state of the object.
Typestates are capable of representing behavioral type refinements such as "method A must be invoked before method B is invoked, and method C may not be invoked in between". Typestates are well-suited to representing resources that use open/close semantics by enforcing semantically valid sequences such as "open then close" as opposed to invalid sequences such as leaving a file in an open state. Such resources include filesystem elements, transactions, connections and protocols. For instance, developers may want to specify that files or sockets must be opened before they are read or written, and that they can no longer be read or written if they have been closed. The name "typestate" stems from the fact that this kind of analysis often models each type of object as a finite state machine. In this state machine, each state has a well-defined set of permitted methods/messages, and method invocations may cause state transitions. Petri nets have also been proposed as a possible behavioral model for use with refinement types.[1]
Typestate analysis was introduced by Rob Strom in 1983[2] in the Network Implementation Language (NIL) developed at IBM's Watson Lab. It was formalized by Strom and Yemini in a 1986 article[3] that described how to use typestate to track the degree of initialisation of variables, guaranteeing that operations would never be applied on improperly initialised data, and further generalized in the Hermes programming language.
In recent years, various studies have developed ways of applying the typestate concept to object-oriented languages.[4][5]
- ^ Jorge Luis Guevara D´ıaz (2010). "Typestate oriented design - A coloured petri net approach" (PDF).
- ^ Strom, Robert E. (1983). "Mechanisms for compile-time enforcement of security". Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages - POPL '83. pp. 276–284. doi:10.1145/567067.567093. ISBN 0897910907. S2CID 6630704.
- ^ Strom, Robert E.; Yemini, Shaula (1986). "Typestate: A programming language concept for enhancing software reliability" (PDF). IEEE Transactions on Software Engineering. 12. IEEE: 157–171. doi:10.1109/tse.1986.6312929. S2CID 15575346.
- ^ DeLine, Robert; Fähndrich, Manuel (2004). "Typestates for Objects". ECOOP 2004 – Object-Oriented Programming. Lecture Notes in Computer Science. Vol. 3086. Springer. pp. 465–490. doi:10.1007/978-3-540-24851-4_21. ISBN 978-3-540-22159-3.
- ^ Bierhoff, Kevin; Aldrich, Jonathan (2007). "Modular typestate checking of aliased objects". Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems, languages and applications. Vol. 42. pp. 301–320. doi:10.1145/1297027.1297050. ISBN 9781595937865. S2CID 9793770.