Beyond-Regular Typestate
Ashish Mishra, Y. N. Srikant

TL;DR
This paper introduces Beyond-Regular Typestate (BR-Typestate), an extension of regular typestates capable of modeling non-regular properties in programs and protocols, with a formal system and a prototype typechecker.
Contribution
It presents a new expressive typestate system, BR-Typestate, along with formal proofs of soundness and a prototype implementation for verifying complex properties.
Findings
BR-Typestate can model non-regular properties
Prototype typechecker verifies real-world properties
System is proven sound and tractable
Abstract
We present an extension for regular typestates, called Beyond- Regular Typestate(BR-Typestate), which is expressive enough to model non-regular properties of programs and protocols over data. We model the BR-Typestate system over a dependently typed, state based, impera- tive core language, and we prove its soundness and tractability. We have implemented a prototype typechecker for the language, and we show how several important, real world non-regular properties of programs and protocols can be verified.
| (program) | (P) | ::= | in main |
| (state definition) | (state) | ::= | state S case of S { |
| (declaration) | (d) | ::= | |
| (method-decl) | (method) | ::= | ()[] { field; method; stmt; e } |
| (field-decl) | (field) | ::= | (var val) f |
| (type-decl) | (type) | ::= | () |
| (typeFamily-decl) | (typefam) | ::= | type |
| (statement) | (stmt) | ::= | let x = e in stmt |
| let x̂.f = e in stmt | |||
| e e in stmt | |||
| match (e : S) | |||
| while [] (, ) | |||
| case e { e } | |||
| (expression) | (e) | ::= | x x̂ new S() new S () |
| e.m() | |||
| e ; e | |||
| c | |||
| (const) | (c) | ::= | boolliteral intliteral stringliteral |
| (permission) | (a) | ::= | unique (1) shared (2) immutable (-1) |
| (type context) | () | ::= | , |
| () | ::= | x : e : d : P : : | |
| (heap) | () | ::= | , |
| () | ::= | x, x̂ value | |
| (value) | value | ::= | c d new S() new S () |
| (type) | () | ::= | void int bool string |
| S | |||
| (typestate transition) | |||
| (function type) | |||
| (method type) | [] | ||
| (a, ) | |||
| (dependent function type) | (, s : S). | ||
| (Type Family-I ) | (, s). | ||
| (Dependent Terms Family) | ::= | ||
| (Presburger Formula) | ::= | b | |
| (Boolean Expression | (b) | ::= | true false i == j i == int |
| (Arithmetic Expression) | (i) | ::= | c v c * a + - i |
| (variable name) | x , x̂ this | ||
| (field name) | f | ||
| (method name) | m , main | ||
| (type family name) | |||
| (state name) | S | ||
| (abstract locations) |
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · semigroups and automata theory
11institutetext: Indian Institute of Science,
Bangalore, India.
%%␣(feature␣abused␣for␣this␣document␣to␣repeat␣the␣title␣also␣on␣left␣hand␣pages)%%␣the␣affiliations␣are␣given␣next;␣don’t␣give␣your␣e-mail␣address%%␣unless␣you␣accept␣that␣it␣will␣be␣published{ashishmishra,srikant}@csa.iisc.ernet.in
Authors’ Instructions
Beyond-Regular Typestate
Ashish Mishra Y. N. Srikant
Abstract
We present an extension for regular typestates, called Beyond-Regular Typestate(BR-Typestate), which is expressive enough to model non-regular properties of programs and protocols over data. We model the BR-Typestate system over a dependently typed, state based, imperative core language, and we prove its soundness and tractability. We have implemented a prototype typechecker for the language, and we show how several important, real world non-regular properties of programs and protocols can be verified.
Keywords:
Typestate, Dependent Type, Non-Regular Program Properties, Verification
1 Introduction
To quote Strom and Yemini, the originator of the Typestate [16]- “while type of data defines what operations are allowed on data for the life time of the data, typestate defines which operations are valid in a given context or state of the data”. Typestates have been a useful concept to model and reason about the stateful effect systems [8, 13] from varied domains. Consider the Buffer State (analogous to a class in Object Oriented paradigm) in Figure 3, with the allowed operations add, remove and print. Types can enforce what operations are allowed on data. However, since the types associated with a datum is immutable, it can not model program properties such as, add or remove from the buffer, only if the buffer is in open state. Typestates associate such mutable types to data objects. Typestate example in Figure 3 defines two sub-typestates of the earlier Buffer state, OpenBuffer and ClosedBuffer. The open(close) operation transits the ClosedBuffer(OpenBuffer) to open(close) state. Figure 3 shows a regular typestate property automaton for Figure 3. Normally, these typestate properties are modeled and enforced using types [16, 12], or could be a feature of the language and enforced statically or at runtime [1].
Now, let us consider a slightly richer example of a Buffer object shared between a producer and a consumer process. The buffer provides library methods produce and consume to these processes. An important runtime property which a producer-consumer model like this must adhere to is- “At any time during the execution the number of items put into the Buffer must be greater than or equal to the number of items consumed from the Buffer”. At the same time, the items can be produced or consumed only when the Buffer is in Open state.
Figure 4 shows a multiple counter machine [11] modeling such a producer consumer problem over a buffer. The machine’s states model the states of the Buffer. The number of items produced and consumed are captured using two counters. A transition in the machine is of the form (), where is an action (like produce or consume) and , is the guard condition for the transition, requiring and guaranteeing . The property stated above could be defined as an invariant on such a machine ( in this case).
The language needed to express and enforce this program property is context-free and thus the regular Typestate lacks expressiveness to model such a property [12].
Figure 6, contains the source for a simple Producer Consumer model over a Buffer as described, in our dependently typed language (described later). The State has a Buffer field and a set of methods open, produce, consume, close. Each field is annotated with its type which could be a user defined dependent type [3], dependent on the runtime values of some dependent term.
Typestates are modeled as instances (line 3) of user defined dependent type families (line 2). Each method has a Hoare style pre and post constraints, which are modeled as a special change type “” that restricts the operations allowed on an object thereby simulating the guarded transitions of the counter machine for the property described earlier. For example, the annotations on method produce in state ProducerConsumer, restricts the production of items to the input Buffer object buf only if it is in open(OB) state and the number of items produced are greater than or equal to the number of items consumed from buf.
A typestate in our model is a predicate over object States (a regular Typestate) and an extra set of Presburger formulas. Given these dependently typed annotations with dependent terms coming from a restricted domain, we can mechanically verify that every well typed method and (in turn the whole program) satisfies the annotated pre-condition and guarantees the annotated post-condition. With such an extension, we can model and enforce the guards of multiple counter machines and can enforce these beyond regular program properties with static type checking, and we call our extension as Beyond-Regular Typestate (BR-Typesatate). There are various languages (both research and real world) which have the full capacity of these dependent types which allow the types to capture and typecheck very complex problems statically. The issue with these languages is that Typechecking for dependent types is undecidable in general (constraint satisfaction is as hard as program equivalence checking) [2], (e.g. Coq, Martin-Löf type theory(underlying NuPrl) etc.).
Figure 5 shows a property violating trace for the main code fragment. We associate a pair (p, c) representing the number of items produced and consumed respectively till now (shown above the state). Thus, the property checking reduces to the reachability problem for a node with () as its constraint, such that . The figure shows one such violating trace for the above code with violating node colored red. The violation is caused due to the possible execution of the OpenBuffer case (line 15) of the match expression.
1.1 Our Contribution
- •
We present the concept of Beyond-Regular Typestate that has higher expressiveness compared to the regular typestate and can model and verify non-regular program properties.
- •
We implement this concept as a restricted dependent type system over an imperative dependently-typed core language inspired by “Typestate-Oriented Programing”, and give the complete formalism for system.
- •
We present a formal proof of the correctness and the decidability of typechecking for our BR-Typestate system. We have also implemented a prototype typechecker for our typestate system.
- •
We model several non-regular real world typestate program properties in our language and verify them using the BR-typestate system.
The outline of the paper is as follows In section 2 we present the formal language and the BR-Typestate system. In section 3, we discuss all the important results and formal properties of our language and the BR-Typestate. Section 4, presents some of the important non-regular program properties and the empirical results that we have generated. Related work and conclusions form the content of sections 5 and 6 respectively.
2 Beyond-Regular Typestate
Beyond-Regular(BR) Typestate extends the regular typestate to depend on auxiliary terms. Theoretically, the base terms on which the typestate could depend could be any expression in the language, but this will cause the reasoning over such a system undecidable. Thus, in our work we restrict these base terms to belong to a smaller and less expressive yet decidable domain of Presburger Arithmetic formulas. The expressions in the language might mutate the type-state of the terms. We also restrict these possible mutations so as to make the dependent base terms domain closed under these mutating operations. The utility and the power of these extensions and restrictions will be discussed in detail in section 3.
With the intuitive informal understanding of the concept of BR-Typestate, now we present a more formal definition for it-
Definition 1 (Beyond-Regular Typestate)
A BR-Typestate BR-ts for an object a, is represented as and is defined as an instance of a dependent function type family , where is the type of dependent base terms domain, (Presburger Formulas) in our concrete typestate system and , is the type of the finite state set available in regular typestate. A typestate will be some member of this type family for a given dependent base term and a given state.
Thus each node along with the universal invariant in Figure 7, represents a BR-ts for a Buffer object. Thus a given node with a state open and (p, c) pair as (c1, c2) represents a BR-ts .
2.1 Core Language
2.1.1 Syntax
We present a small, core language, inspired by and built upon the ideas from [1, 4, 12]. The language is a state oriented, statically typed imperative programming language with restricted dependent types. The language also has States in place of Classes, along with fields, methods, and variables. We have highlighted the new features of the language as compared to the earlier typestate oriented programming languages and typestate works in Table 1. The language allows definitions of user defined dependent function type family(typefam), and instantiations of these functions with particular dependent terms(type). These type families and type instantiations let the programmer define types dependent on terms coming from the domain () and thus allows modeling of BR-Typestates. Moreover, it gives the type system its power to express any possible trace generated by a multiple counter machine (discussed in section 3). The syntax allows to annotate each method declaration with the Pre and Post BR-Typestate values for parameters and the environment(method in the Table 1). The Pre and Post typestates are represented as typestate transition type (). The language requires invariants to be provided explicitly with a while statement. This assumption is crucial for guaranteeing the termination of the BR-Typestate type-checking since the traces generated by the dependent typesystem are possibly infinite length (the type system can simulate a multiple counter machine). In section 3 we discuss the automatic inference of such invariants for some particular subclass of program properties.
Instantiation of States using a novel new expression, parameterized by a presburger formula(new S()) is possible. This creates a new object value with the associated BR-typestate parameterized with . Sequential composition is standard as in any imperative language. The static types in the language are either primary types, a state S, a function type () or a (permission, type) pair **(**a, ). Besides this, there are special types defining a BR-Typestate instance and its transition. A BR-typestate of a variable, reference or a value is an instance (). of a dependent function type family . The BR-Typestate transition is defined by a typestate transition type() or a method type(), which includes a function type and a collection of typestate transition types over parameters and environment variables. Finally, the dependent terms() of dependent types are either a normal presburger formula or a closed bounded presburger formula. A presburger formula has a standard definition of linear logical constraints over arithmetic addition and constant multiplication terms.
Managing aliases is as imperative in BR-Typestate as is in regular typestate [1, 12]. To correctly capture the typestate changes in an imperative language, the changes across any possible aliases must be captured. We use the permission system similar to the earlier works on regular typestates which are effective in our current type system as well. There are three permissions, unique (a unique reference to the object) represented by “1”, shared (atleast two distinct references) represented by “2” and immutable represented by “-1”. Typing rules for permissions are skipped in view of limited space.
2.1.2 Operational Semantics of the Core Language
We present a big step operational semantics for the core-language in the appendix section in the view of limited space. The abstract state of the program is defined as a pair (), two variable to value maps mapping reference variables to abstract locations and value variables to values respectively. The big step semantics are presented as judgments . Such a judgment states that an expression evaluates in the program state , to an abstract value and changes the program state to in the process. If the expression does not evaluate to a value (like, statements), the judgment drops the returned value . Interested readers should refer Appendix, section 7.1 for these semantic rules in Figure 13 and 14 along with their detailed explanation.
2.1.3 Typing Rules
Type Formation
The static dependent type system enforces the type and typestate safety. Figures 9, 10 and 11 presents the dependent typing rules for language expressions, well formedness of method, field and state declarations, and subtyping relations respectively. Figure 8 presents the standard formation, introduction, computation and other related rules for dependent type family. Each judgment in these rules is of the form . It states that in the given typing context and dependent base terms constraint environment (ref. table 1), the expression is well typed and has a type and the typing of the expression updates the to . Any well formed type has a kind which we model as in our type system. Here we discuss in detail only the important and non-standard typing rules in view of limited space, rest are easy to follow. The T-DepFam-F rule in Figure 8, states that a dependent type family could depend on a pair (, ) of a presburger formula based constraint and a state from the finite state set respectively. The rule states, if has a well formed type in the environment and if has a well formed type S, in the environment extended with (), then the type family is well formed. The type system requires to be the type of Presburger Arithmetic formula. The T-DepFam-I and T-DepFam-C are standard introduction and the computation rules for the type family. The next rule T-DepFam-C-Eq defines the rule for equality of two dependent type family instances. It states that two instances of dependent family type are equal iff their dependent base terms are equal component wise. The final rule T-Eq states that if two types are equal as per the tying rules then the type system does not differentiates between them.
Expression Typing
We discuss the most important typing rules. The rule (T-new-Dep) states the typing rule for instantiating a state with initial BR-Typestate. It states, that if the state being instantiated is a well formed declaration(present in State Table, ST), and the presburger formula passed as parameter is well formed, then the expression has a dependent type instance . The rule also checks the well typedness of the dependent type instance and updates the constraint environment to .
The rule (T-update) is the explicit typestate update rule. It first typechecks the right hand expression in the input context and constraint environment and updates the context and the environment. It then checks and updates the type of the left hand expression to the type of the . The earlier type of is discarded, in this sense the Update expression performs a strong type update. The rule for match expression (T-match) assigns an arrow type to the match expression, where the type of the match conditional expression is and is a type union over the types for each case expression body. The final constraint environment is a conjunction of the constraints imposed by each case expression body .
The (T-mcall) rule typechecks the base expression in the pre- context () and confirms it is an dependent type instance (simple state type can be seen as a constant dependent type ). It then typechecks base expression type, the environment variables type and the actual parameters type against the annotated method type, given by the auxiliary mtype routine. Each parameter is checked in a sequentially extended context finally checking the method body . The rule ultimately updates the post type of each expression as per the annotated post type in the method type.
The (T-while) rule checks that the conditional expression is of type bool and it updates the incoming environment to , it then validates the associated invariant in . It typechecks the body of the while expression while is true () and confirms whether invariant holds at the end of the while body(). Finally it validates the invariant when the conditional is false at the exit of the loop.
Field, Method and State Well Formedness
Figure 10, presents the typing rules enforcing and checking the well formedness of fields, methods and states. Each judgment of the form () : () states that the declaration is well formed in the context () and updates the constraint environment to . The method declaration rule (T-m Decl) needs some elucidation, it typechecks list of parameters against the annotated parameter input types, by sequentially updating the context after each such typecheck. For example it checks in the incoming context against the annotated type . It then extends the context (both and ) and further checks the in this extended context. In general it typechecks in the extended context generated by the checking of . Finally, it checks the body of the method declaration in the environment extended by the typechecking of . The typechecking of the environment variables, parameters and the body in corresponding contexts implies the well formedness of the method declaration. The rule for state declaration, T-s Decl straight forwardly checks the well formedness of all the types, fields, methods and states declared in the state.
Subtyping
Figure 11, presents the subtyping rules for the dependent BR-Typestate system. The rule T-Sub-Refl and T-Sub-Trans are standard reflexivity and transitivity rules for subtyping. The rule T-Sub-State defines the subtyping over states, this subtyping relation is definitional in nature such that if sdecl = state S case of {..}, then . The rule T-Sub-Str is the subtyping rule for structural types of the form (), holds iff the permission for is equal to the permission for and recursively (). Rule T-Sub-DepTerm states the subtyping for Dependent term (a presburger formula). It states that if and are well formed presburger formulas then iff satisfaction of implies the satisfaction of . Rule T-DepFam Sub defines the subtyping relation for dependent type family instance. It states, the component wise subtyping relation for the dependent type family instance, i.e. if and then .
3 Discussion and Analysis
3.1 Type Soundness
We present a soundness proof for our BR-Typestate system.
Theorem 3.1 (Progress)
if t : then either
- •
t is a value. OR
- •
* a term t’ such that .*
Proof
We prove the above theorem by induction over the derivation of typing rules for the expressions. (refer Appendix, theorem 7.3 for a detailed proof.)
Theorem 3.2 (Preservation)
if , t : and t t’, then (, ) t’ : and (, ) type.
Proof
The proof is again by the induction on the derivation of . We present the argument about the preservation for an important subset of cases and for others the argument is similar. At each step of the induction we assume by the induction hypothesis(IH) the preservation holds for the sub-derivations and then to complete the induction argument we prove that the argument hold for the current step.(refer Appendix, section 7.3).
Theorem 3.3 (Soundness)
The typestate system presented in section 2 is sound. Formally, if a term t is a well typed term in our typestate system, then it will never be a stuck term.
Proof
3.2 Expressiveness of BR-Typestate
One crucial question to ask is how expressive is the BR-Typestate system defined earlier. We claim that the language of our type system for BR-Typestate(the language generated by the labeled transitions system defined by the dependent type system) although restricted contains all possible traces generated by a multiple counter machine [11].
Theorem 3.4 (BR-Typestate Expressiveness)
The language of the type system for BR-Typestate(the language generated by the labeled transitions system defined by the dependent type system) contains all possible traces generated by a multiple counter machine.
Proof
The proof is by reducing our dependent type system to a labeled transition system (), modeling a multiple counter machine using another labeled transition system () and then showing that simulates .(refer Appendix, section 7.2).
3.3 Decidability of Typecheking BR-Typestate
The typecheking problem for the BR-Typestate is reducible to constraint solving over Presburger Arithmetic formulas. The decidability of the validity problem of Presburger Arithmetic formulas family makes the type checking decidable in our typestate system.
Theorem 3.5 (Reduction to PAF)
For any general typing relation in our typestate system, , such that holds iff is satisfiable.
Proof
The proof is using an inductive argument on the typing derivations of our typestate system. The routine defines the presburger formula for . (Refer Appendix, section 7.4).
3.4 Analysis of the Type Inference Problem
As described earlier the BR-Typestate system assumes that the while syntax is annotated with a loop invariant and we assumed that this is provided by the programmer. This assumption is essential to guarantee termination of our typechecking algorithm. This could be a hard task for a novice programmer and challenging even for an experienced programmer. Fortunately, this burden could be placated in certain special subclasses of programs or properties for which the loop invariants could be effectively computed. The loop invariant inference is based on the efficient and decidable verification results [6, 5, 10] for some known subclasses of multiple counter machines, one of which is the Flat Counter Machine [6]. A multiple counter machine is termed Flat if there is no nested loop in the transition system for the machine. Huber et. al. [6] show that for such machines we can compute a Presburger arithmetic formula representing the fixpoint for a single loop. Since the invariants needed in our case are presburger formulas, we can plug in this fixpoint presburger formula for the loop body in the incoming BR-Typestate at the entry of the loop. For other general class of properties for which such a fixpoint is not effectively computable, we require the programmer to provide an invariant and leave the automatic inference of these invariants for future work.
4 Applications and Results
We now discuss some of the practical real world non-regular program properties which we are able to typecheck and enforce through our Typestate system.
DYCK languages are the languages of balanced parentheses. An example string of a DYCK language is “()(())”.
Definition 2
DYCK language Formally, let ={(,)} be an alphabet consisting of the left and right parentheses. Given word u over , let be the number of occurrences of the left parentheses in u minus the number of occurrences of the right parentheses in u. A word u over is said to be a word of well-balanced parentheses, iff
- •
(u) = 0, and
- •
0 for any prefix v of u.
The DYCK language forms the basis of various constructs in programming languages, Internet domain and other fields. For example, markup languages like html, xml, etc., require the programs to be a string of balanced opening and closing elements. Figure 12 shows a counter machine modeling a DYCK language. The source in our core language captures the states and guards of such machine and skipped due to space limitation.
Definition 3
Assume Guarantee An important class of program properties which needs to be verified are the assume-guarantee properties. These are the properties in which a component (e.g. a function) of the system is specified in terms of the assumptions it makes about its environment (the assume component) and the properties it guarantees about its behavior. The property is naturally represented as .
Assume-guarantee properties are non-regular and hence could not be modeled and enforced using regular typestates. The BR-Typestate by definition models such properties by annotating methods with pre and post constraints. The method assumes certain constraints() to be satisfied(assume) by the environment and in turn guarantees the output state to satisfy certain constraints((), guarantee). Thus the Change Type naturally expresses an assume guarantee property like , such that and .
Definition 4
Uniform Inevitability Problem The uniform inevitability problem says: there exists some rank n, such that every computation sequence of length greater than n satisfies some proposition P at rank n. The property has been shown to be non-expressible by finite automaton [7] thus could not be enforced using regular typestate.
We can model and enforce a variant of Uniform Inevitability problem for a given rank n in BR-Typestate. Thus for a given rank n and a proposition P, we guarantee that a well typed program satisfies -“for all the the paths in the program of length greater than or equal to n, the property P holds”.
Definition 5
Train speed control algorithm The train speed control algorithm controls the speed of the train and guarantees the collision free running of the trains. A train could be in one of the four states viz. ontime, braking , late or stopped. A safety property for such a control system could be defined as - “the train is never late (or early) by more than 20 seconds”. The speed control system is regulated via counters keeping track of number of beacons b passed on the rails and a global clock ticks s, besides this there is another counter which starts in the braking state and counts the ticks during breaking state d. Each state is defined as - The train is ontime iff , its late iff , its early iff finally, when , the train is on time again.
One property of interest to avoid collisions is- , which could not be enforced using regular typestate. We modeled and enforced this property in our BR-Typestate system. A counter machine for the train speed control protocol is shown in Appendix, Figure 15.
Besides the properties described so far in the work, we modeled and enforced a set of other non-regular program properties like (1) checking that any path in the program is in language .(2) Classic static array bound checking etc.. None of these could be expressed and enforced using regular typestate.
5 Related Work
Our core-language is inspired by and built-upon the Typestate Oriented Programming languages works [1, 4] but, the BR-Typestate has a static type system over the core language rather than enforcing the typestate in the language and we use a dependent type system to implement it. Modular typestate for object-oriented programs [12] models the typestates as predicates over object and handle the issues related to subclasses. This handles regular typestate only. We leave modular BR-Typestate for future research wok. Extended Static Checking (ESC) for Java [9] is based on first order logic and general theorem proving. Although ESC is expressive, it does not provide or aim for the decidability and the soundness properties of their static checking, while we show our BR-Typestate system to be sound and our static dependent typechecking to be decidable. The domain of dependently typed extensions for languages [18, 17, 15, 14] is also related. These works are some restricted form of dependent types, but our work with a Presburger arithmetic domain as constraint and a core state oriented, imperative language differs from these. The idea of restricting the domain for dependent terms follows from Xi et. al. [18, 17], but unlike them we use a decidable class of Presburger formulas for which the exact typechecking and subtyping is decidable and even inferable in certain cases. Liquid types [15] and other refinement types associate invariants about the runtime values with the data using dependent types and statically verify these invariants. Their emphasis is primarily on the automatic inference of these invariants, compared to these, we focus on increasing the expressiveness of regular typestates, yet keeping the exact typechecking decidable by choosing a decidable logic family as dependent terms. Moreover, while they take a conservative approach of subtyping by embedding the implications of their subtyping rules into a decidable logic, we restrict the dependent terms themselves to a decidable logic fragment there by making the exact typechecking problem decidable. Nathaniel et. al. [14]present a constrained type for an immutable state of a Class, and this work is strictly less expressive than our work where we can model and typecheck invariants on any data of the program.
6 Conclusion
We have tried to overcome the expressive limitations of regular typestate, by defining the concept of BR-Typestate which is expressive yet decidable. We implemented a restricted dependent type system over a state based, imperative core language. We proved important soundness and decidability results for BR-Typestate and corroborated its effectiveness by verifying several real world non-regular properties.
7 Appendix
7.1 Operational Semantics of the Core Language
The abstract state of the program is defined as a pair (), two variable to value maps mapping reference variables to abstract locations and value variables to values respectively. The big step semantics are presented as . Such a judgment states that an expression evaluates in the program state , to an abstract value and changes the program state to in the process. If the expression does not evaluate to a value (statements), the judgment removes the returned value . Figure 13 presents these semantic rules for the language. Some of these judgments are self explanatory, while the most interesting ones, most closely relevant to the typestate and BR-Typestate are given by the rules mcall, let, match, update, and while. mcall has a call by value semantics. It checks that the receiver reference is mapped to a non-null (null is a special location) location and then creates an extended program state mapping each formal parameter expression to the values of the corresponding actual parameters and it then evaluates the body of the called method in this new extended state to change the state to . The match expression evaluates the match expression and further evaluates each of the case expressions in this new program state returning , and possibly changing the state to (). Since, the match expression could match to any of the possible case expression, we create an over-approximate value for state of the system post completion of the rule. Thus , is a union over all the state maps generated by each of the case expressions. The returned value is one of the any possible returned value, thus this can bee seen as an indexed set of values, indexed over the case expression . The update rule, refer Figure 14 evaluates the source expression of the update expression, changing the state to and updates the fields of the target expression , { } by the values of the corresponding fields from the source expression . The final state is the new updated state with updated maps for each field of and the itself. The while rule semantics depend on the value of the conditional expression , if the the condition evaluates to false (while-false) while updating the state to during evaluation of the , the expression evaluates the next expression (or statement) after the while body. The case for true condition (while-true) is much complex,which evaluates the body of the while statement , in the updated environment and evaluates the next expression , only in the new state (), which is obtained after a fix point for the loop is reached.
7.2 Expressiveness of the BR-Typestate type system
Definition 6 (Labeled Transition System)
A labeled transition system over alphabet is defined as a tuple , where is a possibly infinite but countable set of states, is a set of final states, is a transition relation over states on action set and is a labeling function from states to the alphabet set.
Definition 7 (BR-Typestate LTS)
We construct an LTS := such that-
- •
, where represents a Presburger Formulas in the dependent type system while the PS is finite or infinite set of property states, given as dependent terms in our type system. Thus in a set theoretic sense a state conceptually is equal to a dependent type instance in our type system dependent on .
- •
is the set of actions which is the set of transition over the types. The types , and form the action set for . Note that these typing rules only allow presburger arithmetic transitions.
- •
The labeling function is trivial and returns the formula and state s for a given state.
- •
The transition relation - For a given state defined by () and a given action is defined as-
- –
if a = or , with then ((), , ) .
- –
if a = , with and then ((), ) and ((), ) .
We first define a multiple counters automata formally and then present an LTS for such a system. Finally we present a formal proof for simulating the LTS for this Multiple Counters Automata.
Definition 8 (Multiple Counters Automata)
A multiple counters automata is a tuple where-
- •
Q is a finite set of states.
- •
is an initial state
- •
is the finite set of counter variable names, is the set of primed counter variable names.
- •
is the set of guards built on the alphabets . A member of is a conjunction of atomic formulas of the forms , where and
Definition 9 (Multiple Counters Automata LTS)
We construct an LTS := such that -
- •
, such that if , then (q, ) and (q’, ) .
- •
. This defines set of formulas from (), which encode the actions of the LTS.
- •
.
- •
, such that
- •
Definition 10 (Simulation)
Given two LTS := and := . A relation is a simulation if and following holds-
- •
iff then . and
- •
iif then , such that . and
- •
.
If then we say that state simulates state .
Definition 11 (Simulation between LTS)
Let and be start states for two LTS and respectively. simulates iff , where is a simulation relation as defined above.
Using these definition now we state and prove important simulation property regarding and .
Theorem 7.1
If is an LTS for the BR-Typestate type system and another LTS for the Multiple Counters Automata, then simulates the LTS . Formally. . and start states and of and respectively, then .
Proof
The proof is an inductive constructive proof on transition relation over and over finite action set.
Base case -If then by construction we have a state , such that and .
Induction Hypothesis - Let, for any state , then such that .
Inductive Step- By IH, , thus by the definition of simulation, states reachable from . Thus we look at the transitions from and . transitions , from , where we can always construct a transition , where such that and . Thus . Hence by induction, such that .
Corollary 1
* and thus by definition 11 simulates .*
7.3 Proof of Soundness of Type System
Theorem 7.2 (Progress)
if t : then either
- •
t is a value. OR
- •
* a term t’ such that .*
We prove the above theorem by induction over the derivation of typing rules for the expressions.
Proof
The base cases exists for terms which are values, viz. T-New, T-New-Dep and T-mDecl. The case T-Var is trivially satisfied as the term is not typable in an empty context. The interesting cases to consider are T-Let, T-Fref, T-Update, T-Match, T-Case and T-While.
- •
T-Let - t := let x = in e. By IH either is a value in which case t reduces to the substitution [value() / x]e, or in which case t t’, such that t’ := let x = in e.
- •
T-Fref - t := let x̂.f = in e. The argument for the T-Let holds in this case too.
- •
T-Update - t := e ; , By IH either is a value, in which case t is reduced to [value() / e], or thus t t’, such that t’ := e .
- •
T-Match - t := match , By the rule T-Match , , by IH, either is a value in which case such that State() State(), and t t’, where t’ = body of case . Else, if , t t”, where t” := match .
- •
T-Case - The argument of T-Case is standard , where the expression is reduced to the body of the case expression.
- •
T-mcall - t := e.m(, ,…,)- Reduced to cases -
- –
By IH on the expression e and each of , e and is a value, in this case t is reduced to [e/this , /], where this is the base object and each of are the formal argument in the method declration and is the body of the method m.
- –
if e is a value and , such that , then t t’ with t’ := e.m(, ,… , …,).
- –
if e e’ then t t’ with t’ := e’.m(, ,…, ).
- •
T-While - t := while [] (, ); stmt , this is a standard While case with case wise split for = true and false.
Theorem 7.3 (Preservation)
if , t : and t t’, then (, ) t’ : and (, ) type.
Proof
The proof is by the induction on the derivation of We present the argument about the preservation for an important subset of cases and for others the argument is similar. At each step of the induction we assume that by Induction hypothesis, the preservation lemma holds and then to complete the induction argument we prove that the argument hold for the current step.
- •
T-New, T-New-Dep, T-mDecl, since these are values and thus t’ such that t t’ and thus the argument vacuously holds for these typing derivation rules.
- •
T-F-Ref , t := e.f : type, now by IH if e e’ then t t’, where t’ := e’.f and e’ is well typed. By T-F-Ref (), such that and . Let sdecl = state case of {… ..}, thus the type of t’ := .
- •
T-Update, t := e e’ and t : , if e’ e”, then t t’ and t’ := e e”. By IH if e’ : then after e’ e”, e” : . Thus by T-update, t’ : ).
- •
T-match, t := match , t : . There are two possible ways of reduction of t t’-
- –
If , then t t’, such that t’ := match . By IH if then . By T-match, .
- –
If for some , then t t’, such that t’ := match . By IH, if then . By T-match, let = then .
- •
T-let, t := let x = in e. There are two distinct possibilities of reduction of t t’-
- –
If , by IH . Let e : , then t’ := let x = in e and t’ : .
- –
If e e’, by IH . thus for t t’, t’ : .
- •
T-mcall, t := e.m(). There are two distinct possibilities of reduction of t t’-
- –
e.m(…) e’.m(…), if e e’. By IH, let e’ : . By T-mcall, let then t’ : .
- –
e.m(…,,…,) e.m(…,,…,) for some if . By IH : . By T-mcall, let , then t’ : .
- •
T-while, while [] () {e}. Again two distinct possible way of reduction of t t’-
- –
If , by T-while , and let , then t’ : .
- –
If e e’, By IH , then t’ : .
7.4 Proof of Decidability of Typechecking
The typecheking problem for the BR-Typestate, is always reducible to constraint solving over Presburger Arithmetic formulas. Since the Presburger Arithmetic has a decidable and tractable validity problem, this makes the type checking decidable in our typestate system.
Theorem 7.4 (Reduction to PAF)
For any general typing relation in our typestate system, , such that holds iff is satisfiable.
Proof
The proof is using an inductive argument on the typing derivations for formation, well formedness and subtyping in our typestate system. The routine defines the presburger formula for . We consider here only the base types and other complex types and show the PAF for each of these.
- •
Base case : primary type , = = .
- •
Case :: , let define a variable for the state S, then the formula .
- •
Case :: , by IH let = and = , then = .
- •
Case :: , by IH let = and = , then = .
- •
Case :: , By expression typing rules, . By IH let = and = and , then = .
- •
Case :: , the case is similar to the above.
7.5 Train Speed-Control Protocol
he train speed control algorithm controls the speed of the train and guarantees the collision free running of the trains. A train could be in one of the four states viz. ontime, braking , late or stopped. Thus a safety property for such a control system could be defined as - “the train is never late (or early) by more than 20 seconds”. The speed control system is regulated via counters keeping track of number of beacons b passed on the rails and a global clock ticks s, besides this there is another counter which starts in the braking state and counts the ticks during breaking state d. Each state is defined as - The train is ontime iff , its late iff , its early iff finally, when , the train is on time again.
One property of interest to avoid collisions is- , which could not be enforced using regular typestate. We present a counter machine for the train speed control protocol in appendix section figure 15.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] Jonathan Aldrich, Joshua Sunshine, Darpan Saini, and Zachary Sparks. Typestate-oriented programming. In Proceedings of the 24th ACM SIGPLAN Conference Companion on Object Oriented Programming Systems Languages and Applications , OOPSLA ’09, pages 1015–1022, New York, NY, USA, 2009. ACM.
- 2[2] Lennart Augustsson. Cayenne—a language with dependent types. In Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming , ICFP ’98, pages 239–250, New York, NY, USA, 1998. ACM.
- 3[3] Ana Bove and Peter Dybjer. Language engineering and rigorous software development. chapter Dependent Types at Work, pages 57–99. Springer-Verlag, Berlin, Heidelberg, 2009.
- 4[4] Sarah Chasins. Efficient implementation of the plaid language. In Proceedings of the ACM International Conference Companion on Object Oriented Programming Systems Languages and Applications Companion , OOPSLA ’11, pages 209–210, New York, NY, USA, 2011. ACM.
- 5[5] Hubert Comon and Véronique Cortier. Flatness is not a weakness. In Proceedings of the 14th Annual Conference of the EACSL on Computer Science Logic , pages 262–276, London, UK, UK, 2000. Springer-Verlag.
- 6[6] Hubert Comon and Yan Jurski. Multiple counters automata, safety analysis and presburger arithmetic. In Proceedings of the 10th International Conference on Computer Aided Verification , CAV ’98, pages 268–279, London, UK, UK, 1998. Springer-Verlag.
- 7[7] E.Allen Emerson. Uniform inevitability is tree automation ineffable. Information Processing Letters , 24(2):77 – 79, 1987.
- 8[8] Stephen J. Fink, Eran Yahav, Nurit Dor, G. Ramalingam, and Emmanuel Geay. Effective typestate verification in the presence of aliasing. ACM Trans. Softw. Eng. Methodol. , 17(2):9:1–9:34, May 2008.
