IEEE Transactions on Software Engineering · 1986 · 624 citations · 0 references
ComputingComputer ScienceCompilersProgramming LanguagesSoftware EngineeringCompiler ConstructionControl-flow AnalysisData-flow AnalysisSoftware Fault ToleranceType CheckingType SystemsDynamic Program AnalysisDynamic Type CheckingRuntime Type CheckingSoftware ReliabilitySoftware Reliability AssessmentSoftware Reliability EngineeringStatic Type CheckingType Analysis
Typestate refines the type system by specifying which operations are allowed in a given context, thereby enabling detection of errors such as using uninitialized variables or dereferencing freed pointers. The authors introduce typestate as a new programming language concept, define it, provide application examples, and demonstrate how typestate checking can be integrated into a compiler. Typestate tracking is a compile‑time program analysis that identifies syntactically legal but semantically undefined execution sequences, and the authors illustrate its implementation within a compiler. The authors report that typestate checking enhances software reliability and influences software structure, and they share their experience using a high‑level language that incorporates typestate checking.
The authors introduce a new programming language concept, called typestate, which is a refinement of the concept of type. Whereas the type of a data object determines the set of operations over permitted on the object, typestate determines the subset of these operations which is permitted in a particular context. Typestate tracking is a program analysis technique which enhances program reliability by detecting at compile-time syntactically legal but semantically undefined execution sequences. These include reading a variable before it has been initialized and dereferencing a pointer after the dynamic object has been deallocated. The authors define typestate, give examples of its application, and show how typestate checking may be embedded into a compiler. They discuss the consequences of typestate checking for software reliability and software structure, and summarize their experience in using a high-level language incorporating typestate checking.