Beyond-Regular Typestate

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.

Tables

Table 1. Table 1: Core Language Syntax

(program)	(P)	::=	$stat{e}_1,stat{e}_2,\dots stat{e}_n$ in main
(state definition)	(state)	::=	state S case of S { $\overline{d}\}$
(declaration)	(d)	::=	$method\mid field\mid state\mid typefam\mid type$
(method-decl)	(method)	::=	${\tau }_r$ $m_i$ ($\overline{{\tau }_{ai}\gg {\tau }_{a{i}^{\prime }}{a}_i}$)[$\overline{{\tau }_j\gg {\tau }_{j^{\prime }}{a}_j}$] { field; method; stmt; e }
(field-decl)	(field)	::=	(var $\mid$ val) $\tau$ f
(type-decl)	(type)	::=	$\gamma$ (${\varphi }_i,s_i$)
(typeFamily-decl)	(typefam)	::=	type $\gamma {\Pi }_{\left(\varphi :\Phi ,s:state\right)}.\tau$
(statement)	(stmt)	::=	let x = e in stmt
			$\mid$ let x̂.f = e in stmt
			$\mid$ e $\leftarrow$ e in stmt
			$\mid$ match (e : S) $\overline{\text{case e {e}}}$
			$\mid$while [$\exists .\varphi$] ($e_1:Bool$, $e_2$)
			$\mid$ case e { e }
(expression)	(e)	::=	x $\mid$ x̂ $\mid$ new S() $\mid$ new S ($\varphi :\Phi$)
			$\mid$ e.m($e_1,e_2,\dots ,e_p$)
			$\mid$ e ; e
			$\mid$ c
(const)	(c)	::=	boolliteral $\mid$ intliteral $\mid$ stringliteral
(permission)	(a)	::=	unique (1) $\mid$ shared (2) $\mid$ immutable (-1)
(type context)	($\Gamma$)	::=	$\bullet$ $\mid$ $\delta$, $\Gamma$
	($\delta$)	::=	x : $\tau$ $\mid$ e : $\tau$ $\mid$ d : $\tau$ $\mid$ P : $\tau$ $\mid$ $\tau$ : $\star$
(heap)	($\Theta$)	::=	$\bullet$ $\mid$ $\theta$, $\Theta$
	($\theta$)	::=	x, x̂ $\mapsto$ value
(value)	value	::=	c $\mid$ d $\mid$ new S() $\mid$ new S ($\varphi :Phi$) $\mid$ $l_i$
(type)	($\tau$)	::=	void $\mid$ int $\mid$ bool $\mid$ string
			$\mid$ S
(typestate transition)			$\mid$ ${\tau }_i\gg {\tau }_j$
(function type)			$\mid$ ${\tau }_1\to {\tau }_2$
(method type)			$\mid$ ${\tau }_1\to {\tau }_2$ [$\overline{{\tau }_i\gg {\tau }_j}$]
			$\mid$ (a, $\tau$)
(dependent function type)			$\mid$ $\Pi$ ($\varphi :\Phi$, s : S).$\tau$
(Type Family-I )			$\mid$ ($\varphi$, s).$\tau$
(Dependent Terms Family)	$\Phi$	::=	$\varphi \mid {\lambda }_{m_1,m_2,\dots m_n}.\varphi$
(Presburger Formula)	$\varphi$	::=	b $\mid$ ${\varphi }_1\wedge {\varphi }_2$ $\mid$ ${\varphi }_1\vee {\varphi }_2$ $\mid$ $\sim \varphi$ $\mid$ $\exists v.\varphi$
(Boolean Expression	(b)	::=	true $\mid$ false $\mid$ i == j $\mid$ $i\le j$ $\mid$ $i\ge j$ $\mid$ $i\ne j$ $\mid$ i == int
(Arithmetic Expression)	(i)	::=	c $\mid$ v $\mid$ c * a $\mid$ $i_1$ + $i_2$ $\mid$ - i
(variable name)	x , x̂ this
(field name)	f
(method name)	m , main
(type family name)	$\gamma$
(state name)	S
(abstract locations)	$l_i$

Full text

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 ($\alpha,G(\phi_{i},\phi_{2})$), where $\alpha$ is an action (like produce or consume) and $G(\phi_{1},\phi_{2})$, is the guard condition for the transition, requiring $\phi_{1}$ and guaranteeing $\phi_{2}$. The property stated above could be defined as an invariant on such a machine ($p\geq c$ 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 “$\gg$” 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 ($p_{i},c_{i}$) as its constraint, such that $p_{i}<c_{i}$. 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 $a@ts$ and is defined as an instance of a dependent function type family $\Pi_{(\phi:\Phi,s:S)}.\tau$, where $\Phi$ is the type of dependent base terms domain, (Presburger Formulas) in our concrete typestate system and $S$, 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 $\forall nodes,p\geq c$ 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 $[\{(p==c1,c==c2)\wedge c1\geq c2\}/\phi,open/S]\tau$.

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 ($\Phi\times states$) 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 ($\tau_{i}\gg\tau_{j}$). 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($\phi:\Phi$)) is possible. This creates a new object value with the associated BR-typestate parameterized with $(\phi,S)$. 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 ($\tau_{1}\rightarrow\tau_{2}$) or a (permission, type) pair **(**a, $\tau$). 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 ($\phi,s$).$\tau$ of a dependent function type family $\Pi(\phi:\Phi,s:S).\tau$. The BR-Typestate transition is defined by a typestate transition type($\tau_{i}\gg\tau_{j}$) or a method type($\tau_{i}\rightarrow\tau_{2}[\tau_{i}\gg\tau_{j}]$), which includes a function type and a collection of typestate transition types over parameters and environment variables. Finally, the dependent terms($\Phi$) 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 ($\Theta,\Delta$), 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 $(\Theta,\Delta)\vdash e:\rho;(\Theta^{\prime},\Delta^{\prime})$. Such a judgment states that an expression $e$ evaluates in the program state $(\Theta,\Delta)$, to an abstract value $\rho$ and changes the program state to $(\Theta^{\prime},\Delta^{\prime})$ in the process. If the expression does not evaluate to a value (like, statements), the judgment drops the returned value $\rho$. 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 $(\Phi,\Gamma)\vdash e:(\Phi^{\prime},\tau)$. It states that in the given typing context $\Gamma$ and dependent base terms constraint environment $\Phi$ (ref. table 1), the expression $e$ is well typed and has a type $\tau$ and the typing of the expression updates the $\Phi$ to $\Phi^{\prime}$. Any well formed type has a kind which we model as $\star$ 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 ($m$, $s$) of a presburger formula based constraint and a state from the finite state set respectively. The rule states, if $m$ has a well formed type $t$ in the environment and if $s$ has a well formed type S, in the environment extended with ($m:t$), then the type family $\Pi(m:t,s:S).\tau$ is well formed. The type system requires $t$ 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 $S_{1}$ being instantiated is a well formed declaration(present in State Table, ST), and the presburger formula $\phi_{1}$ passed as parameter is well formed, then the expression has a dependent type instance $(\phi_{1},S).\tau$. The rule also checks the well typedness of the dependent type instance and updates the constraint environment to $\Phi\wedge\phi_{1}$.

The rule (T-update) is the explicit typestate update rule. It first typechecks the right hand expression $e_{1}$ 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 $e_{1}$. The earlier type of $e$ is discarded, in this sense the Update expression performs a strong type update. The rule for match expression (T-match) assigns an arrow type $\tau_{1}\rightarrow\tau_{u}$ to the match expression, where the type of the match conditional expression $e_{1}$ is $\tau_{1}$ and $\tau_{u}$ is a type union over the types for each case expression body. The final constraint environment is a conjunction of the constraints $\phi_{i}$ imposed by each case expression body $e_{i}$.

The (T-mcall) rule typechecks the base expression $e$ in the pre- context ($\Phi,\Gamma$) and confirms it is an dependent type instance (simple state type $s_{i}$ can be seen as a constant dependent type $(_{,}s_{i}).\tau$). 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 $e_{m}$. 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 $e_{1}$ is of type bool and it updates the incoming environment $\Phi$ to $\Phi_{1}$, it then validates the associated invariant $\phi$ in $\Phi_{1}$. It typechecks the body of the while expression while $e_{1}$ is true ($\Phi_{1}\wedge(e_{1}==true)$) and confirms whether invariant holds at the end of the while body($\Phi\vDash\exists.\phi$). Finally it validates the invariant when the conditional $e_{1}$ 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 ($\Phi,\Gamma$) $\vdash$ $d$ : ($\Phi^{\prime},\star$) states that the declaration $d$ is well formed in the context ($\Phi,\Gamma$) and updates the constraint environment to $\Phi^{\prime}$. The method declaration rule (T-m Decl) needs some elucidation, it typechecks list of parameters $\overline{e_{i}}$ against the annotated parameter input types, by sequentially updating the context after each such typecheck. For example it checks $e_{1}$ in the incoming context against the annotated type $\tau_{1}$. It then extends the context (both $\Phi$ and $\Gamma$) and further checks the $e_{2}$ in this extended context. In general it typechecks $e_{i}$ in the extended context generated by the checking of $e_{i-1}$. Finally, it checks the body of the method declaration in the environment extended by the typechecking of $e_{m}$. 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 $S_{1}${..}, then $S<:S_{1}$. The rule T-Sub-Str is the subtyping rule for structural types of the form ($a,\tau$), $\tau_{1}$ $<:$ $\tau_{2}$ holds iff the permission $a_{1}$ for $\tau_{1}$ is equal to the permission $a_{2}$ for $\tau_{2}$ and recursively ($\tau_{1^{\prime}}<:\tau_{2^{\prime}}$). Rule T-Sub-DepTerm states the subtyping for Dependent term (a presburger formula). It states that if $\phi_{1}$ and $\phi_{2}$ are well formed presburger formulas then $\phi_{1}<:\phi_{2}$ iff satisfaction of $\phi_{1}$ implies the satisfaction of $\phi_{2}$. 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 $\phi_{1}<:\phi_{2}$ and $s_{1}<:s_{2}$ then $[\phi_{1}/\phi,s_{1}/S].\tau<:[\phi_{2}/\phi,s_{2}/S].\tau$.

3 Discussion and Analysis

3.1 Type Soundness

We present a soundness proof for our BR-Typestate system.

Theorem 3.1 (Progress)

if $\vdash$ t : $\tau$ then either

• •

t is a value. OR

• •

$\exists$* a term t’ such that $t\rightarrow t^{\prime}$.*

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 $\Gamma$, $\Phi$ $\vdash$ t : $\tau$ and t $\rightarrow$ t’, then ($\Gamma^{\prime}$, $\Phi^{\prime}$) $\vdash$ t’ : $\tau^{\prime}$ and ($\Gamma^{\prime}$, $\Phi^{\prime}$) $\vdash$ $\tau^{\prime}$ type.

Proof

The proof is again by the induction on the derivation of $(\Phi,\Gamma)\vdash t:\tau$. 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

By Theorem 3.1 and 3.2

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 ($\mathbb{T}_{br}$), modeling a multiple counter machine using another labeled transition system ($\mathbb{T}_{mca}$) and then showing that $\mathbb{T}_{br}$ simulates $\mathbb{T}_{mca}$.(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 $(\Phi,\Gamma)\vdash t:(\Phi^{\prime},\tau)$ in our typestate system, $\exists.\psi\in PresburgerArithmeticFormula$, such that $(\Phi,\Gamma)\vdash t:(\Phi^{\prime},\tau)$ holds iff $\psi$ is satisfiable.

Proof

The proof is using an inductive argument on the typing derivations of our typestate system. The routine $\psi(\tau)$ defines the presburger formula for $\tau$. (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 $\Sigma_{1}$={(,)} be an alphabet consisting of the left and right parentheses. Given word u over $\Sigma_{1}$, let $D_{1}(u)$ 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 $\Sigma_{1}$ is said to be a word of well-balanced parentheses, iff

• •

$D_{1}$(u) = 0, and

• •

$D_{1}(v)\geq$ 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 $\phi\triangleright\psi$.

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($\phi$) to be satisfied(assume) by the environment and in turn guarantees the output state to satisfy certain constraints(($\psi$), guarantee). Thus the Change Type $\tau_{1}\rightarrow\tau_{2}[\overline{\tau_{i}>>\tau_{i}^{\prime}}]$ naturally expresses an assume guarantee property like $\phi\triangleright\psi$, such that $\tau_{i}\models\phi$ and $\tau_{i}^{\prime}\models\psi$.

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 $s-9<b<s+9$, its late iff $b\in[s-9,s-1]$, its early iff $b\geq s+9$ finally, when $b=s+1$, the train is on time again.

One property of interest to avoid collisions is- $\forall time,\mid b-s\mid\leq 20$, 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 $a^{n}b^{n}$.(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 ($\Theta,\Delta$), two variable to value maps mapping reference variables to abstract locations and value variables to values respectively. The big step semantics are presented as $(\Theta,\Delta)\vdash e:\rho;(\Theta^{\prime},\Delta^{\prime})$. Such a judgment states that an expression $e$ evaluates in the program state $(\Theta,\Delta)$, to an abstract value $\rho$ and changes the program state to $(\Theta^{\prime},\Delta^{\prime})$ in the process. If the expression does not evaluate to a value (statements), the judgment removes the returned value $\rho$. 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 $e_{i}$ 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 $(\Theta_{out},\Delta_{out})$. The match expression evaluates the match expression $e$ and further evaluates each of the case expressions $e_{i}$ in this new program state returning $\rho_{ei}$, and possibly changing the state to ($\Theta_{i},\Delta_{i}$). 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 $(\Theta_{out},\Delta_{out})$, is a union over all the state maps generated by each of the case expressions. The returned value $\oplus\rho_{ei}$ is one of the any possible returned value, thus this can bee seen as an indexed set of values, indexed over the case expression $e_{i}$. The update rule, refer Figure 14 evaluates the source expression $e^{\prime}$ of the update expression, changing the state to $(\Theta^{\prime},\Delta^{\prime})$ and updates the fields of the target expression $e$, { $f_{1},...f_{p}$ } by the values of the corresponding fields from the source expression $e^{\prime}$. The final state is the new updated state with updated maps for each field of $e$ and the $e$ itself. The while rule semantics depend on the value of the conditional expression $b$, if the the condition evaluates to false (while-false) while updating the state to $\Theta^{\prime},\Delta^{\prime}$ during evaluation of the $b$, the expression evaluates the next expression (or statement) $e_{n}$ after the while body. The case for true condition (while-true) is much complex,which evaluates the body of the while statement $e$, in the updated environment and evaluates the next expression $e_{n}$, only in the new state ($\Theta^{\prime},\Delta^{\prime}$), 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 $\mathbb{T}$ over alphabet $\Sigma$ is defined as a tuple $\langle S,A,\rightarrow\pi,F\rangle$, where $S$ is a possibly infinite but countable set of states, $F\subseteq S$ is a set of final states, $\rightarrow\subseteq(S\times A\times S)$ is a transition relation over states on action set $A$ and $\pi:S\mapsto\Sigma$ is a labeling function from states to the alphabet set.

Definition 7 (BR-Typestate LTS)

We construct an LTS $\mathbb{T}_{br}$ := $\langle S_{br},A_{br},\rightarrow_{br},\pi_{br},F_{br}\rangle$ such that-

• •

$S_{br}\subseteq(\Phi\times PS)$, where $\Phi$ 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 $\phi\in\Phi,s\in PS$.

• •

$A_{br}$ is the set of actions which is the set of transition over the types. The types $\tau_{1}\rightarrow\tau_{2}$, $\tau_{i}>>\tau_{j}$ and $\tau_{1}\rightarrow\tau_{2}[\tau_{i}\gg\tau_{j}]$ form the action set for $\mathbb{T}_{br}$. Note that these typing rules only allow presburger arithmetic transitions.

• •

The labeling function $\pi_{br}$ is trivial and returns the formula $\phi$ and state s for a given state.

• •

The transition relation $\rightarrow_{br}$ - For a given state defined by ($\phi_{1},s_{1}$) and a given action $a\in A_{br}$ is defined as-

• –

if a = $\tau_{i}>>\tau_{j}$ or $\tau_{i}\rightarrow\tau_{j}$, with $\tau_{i}:=(\phi_{i},s_{i}).\tau,\tau_{j}:=(\phi_{j},s_{j}).\tau$ then (($\phi_{i},s_{i}$), $(\tau_{i}>>\tau_{j})$, $(\phi_{j},s_{j})$) $\in\rightarrow_{br}$.

• –

if a = $\tau_{1}\rightarrow\tau_{2}[\tau_{i}\gg\tau_{j}]$, with $\tau_{i}:=(\phi_{i},s_{i}).\tau,\tau_{j}:=(\phi_{j},s_{j}).\tau$ and $\tau_{1}:=(\phi_{1},s_{1}).\tau,\tau_{2}:=(\phi_{2},s_{2}).\tau$ then (($\phi_{i},s_{i}$), $(\tau_{i}>>\tau_{j})$ $(\phi_{j},s_{j})$) $\in\rightarrow_{br}$ and (($\phi_{1},s_{1}$), $(\tau_{1}\rightarrow\tau_{2})$ $(\phi_{2},s_{2})$) $\in\rightarrow_{br}$.

We first define a multiple counters automata formally and then present an LTS for such a system. Finally we present a formal proof for $\mathbb{T}_{br}$ simulating the LTS for this Multiple Counters Automata.

Definition 8 (Multiple Counters Automata)

A multiple counters automata is a tuple $(Q,q_{i},C,\delta\subseteq Q\times G(C,C^{\prime})\times Q)$ where-

• •

Q is a finite set of states.

• •

$q_{i}\in Q$ is an initial state

• •

$C$ is the finite set of counter variable names, $C^{\prime}$ is the set of primed counter variable names.

• •

$G(C,C^{\prime})$ is the set of guards built on the alphabets $C,C^{\prime}$. A member of $G(C,C^{\prime})$ is a conjunction of atomic formulas of the forms $x\sharp y+c,x\sharp c$, where $x,y\in C\cup C^{\prime},\sharp\in\{\geq,\leq,=,>,<\}$ and $c\in\mathbb{Z}.$

Definition 9 (Multiple Counters Automata LTS)

We construct an LTS $\mathbb{T}_{mca}$ := $\langle S_{mca},A_{mca},\rightarrow_{mca},\pi_{mca},F_{mca}\rangle$ such that -

• •

$S_{mca}\subseteq Q\times(C\cup C^{\prime})$, such that if $(q,c_{i},c_{i}^{\prime},q^{\prime})\in\delta$, then (q, $c_{i}$) $\in S_{mca}$ and (q’, $c_{i}$) $\in S_{mca}$.

• •

$A_{mca}\subseteq(C\cup C^{\prime})$. This defines set of formulas from ($C\cup C^{\prime}$), which encode the actions of the LTS.

• •

$\rightarrow_{mca}\subseteq(S_{mca}\times A_{mca}\times S_{mca})$.

• •

$\pi_{mca}:S_{mca}\mapsto(C\cup C^{\prime})$, such that $\forall s_{i}\in S_{mca}=(q_{i},c_{i}),\pi_{mca}(s_{i})=(q_{i},c_{i})$

• •

$F_{mca}\subseteq S_{mca}$

Definition 10 (Simulation)

Given two LTS $TS_{1}$ := $\langle S_{1},A,\rightarrow_{1},\pi_{1},F_{1}\rangle$ and $TS_{2}$ := $\langle S_{2},A,\rightarrow_{2},\pi_{2},F_{2}\rangle$. A relation $R\subseteq(S_{1}\times S_{2})$ is a simulation if $\forall,(p,q)\in R$ and $a\in A$ following holds-

• •

iff $q\in F_{2}$ then $p\in F_{1}$. and

• •

iif $(q,a,q^{\prime})\in\rightarrow_{2}$ then $\exists.p^{\prime}\in S_{1}$, such that $(p,a,p^{\prime})\in\rightarrow_{1}$. and

• •

$(p^{\prime},q^{\prime})\in R$.

If $(p,q)\in R$ then we say that state $p$ simulates state $q$.

Definition 11 (Simulation between LTS)

Let $p_{0}$ and $q_{0}$ be start states for two LTS $T_{1}$ and $T_{2}$ respectively. $T_{1}$ simulates $T_{2}$ iff $(p_{0},q_{0})\in R$, where $R\subseteq(S_{1}\times S_{2})$ is a simulation relation as defined above.

Using these definition now we state and prove important simulation property regarding $\mathbb{T}_{br}$ and $\mathbb{T}_{mca}$.

Theorem 7.1

If $\mathbb{T}_{br}$ is an LTS for the BR-Typestate type system and another LTS $\mathbb{T}_{mca}$ for the Multiple Counters Automata, then $\mathbb{T}_{br}$ simulates the LTS $\mathbb{T}_{mca}$. Formally. $\exists Sim$. $Sim\subseteq(S_{br}\times S_{mca})$ and start states $p_{0}$ and $q_{0}$ of $\mathbb{T}_{br}$ and $\mathbb{T}_{mca}$ respectively, then $(p_{0},q_{0})\in Sim$.

Proof

The proof is an inductive constructive proof on transition relation over $\mathbb{T}_{br}$ and $\mathbb{T}_{mca}$ over finite action set.

Base case -If $(q_{0})=(s_{0},c_{0})\in F_{mca}$ then by construction we have a state $p_{0}\in S_{br}$, such that $p_{0}=(c_{0},s_{0})$ and $p_{0}\in F_{br}$.

Induction Hypothesis - Let, for any state $q_{i-2}=(s_{i-2},c_{i-2})\in S_{mca}$, then $\exists p_{i-2}=(c_{i-2},s_{i-2})\in S_{br}$ such that $(p_{i-2},q_{i-2})\in Sim$.

Inductive Step- By IH, $(p_{i-2},q_{i-2})\in Sim$, thus by the definition of simulation, states $(p_{i-1},q_{i-1})$ reachable from $(p_{i-2},q_{i-2})\in Sim$. Thus we look at the transitions from $p_{i-1}$ and $q_{i-1}$. $\forall$ transitions $\alpha_{mca}$, from $q_{i-1}$, where $\alpha_{mca}:=(q_{i-1},(c_{i-1},c^{\prime}{i-1}),q_{i})\in\rightarrow_{mca}$ we can always construct a transition $\alpha_{br}:=(p_{i-1},a_{i},p_{i})\in\rightarrow_{br}$, where $a_{i}=\tau_{i-1}>>\tau_{i}$ such that $\tau_{i-1}=(s_{i-1},c_{i-1}).\tau$ and $\tau_{i}=(s_{i},c^{\prime}_{i-1}).\tau$. Thus $(p_{i-1},q_{i-1})\in Sim$. Hence by induction, $\forall q_{i}\in S_{mca},\exists p_{i}\in S_{br}$ such that $(p_{i},q_{i})\in Sim$.

Corollary 1

$(p_{0},q_{0})\in Sim$* and thus by definition 11 $\mathbb{T}_{br}$ simulates $\mathbb{T}_{mca}$.*

7.3 Proof of Soundness of Type System

Theorem 7.2 (Progress)

if $\vdash$ t : $\tau$ then either

• •

t is a value. OR

• •

$\exists$* a term t’ such that $t\rightarrow t^{\prime}$.*

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 = $e_{1}$ in e. By IH either $e_{1}$ is a value in which case t reduces to the substitution [value($e_{1}$) / x]e, or $e_{1}\rightarrow e_{1^{\prime}}$ in which case t $\rightarrow$ t’, such that t’ := let x = $e_{1^{\prime}}$ in e.

• •

T-Fref - t := let x̂.f = $e_{1}$ in e. The argument for the T-Let holds in this case too.

• •

T-Update - t := e $\leftarrow$ $e_{1}$ ; $e_{n}$, By IH either $e_{1}$ is a value, in which case t is reduced to [value($e_{1}$) / e]$e_{n}$, or $e_{1}\rightarrow e_{1^{\prime}}$ thus t $\rightarrow$ t’, such that t’ := e $\leftarrow e_{1^{\prime}}$.

• •

T-Match - t := match $e_{1}$ $\overline{\textnormal{case}e_{i}}$, By the rule T-Match , $\vdash e_{1}:State$, by IH, either $e_{1}$ is a value in which case $\exists.e_{j}\in\overline{e_{i}}$ such that State($e_{j}$) $<:$ State($e_{1}$), and t $\rightarrow$ t’, where t’ = body of case $e_{j}$. Else, if $e_{1}$ $\rightarrow e_{1^{\prime}}$, t $\rightarrow$ t”, where t” := match $e_{1^{\prime}}$ $\overline{\textnormal{case}e_{i}}$.

• •

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($e_{1}$, $e_{2}$,…,$e_{p}$)- Reduced to cases -

• –

By IH on the expression e and each of $e_{i}$ $1\leq i\leq p$, e and $e_{i}$ is a value, in this case t is reduced to [e/this , $e_{i}$/$x_{i}$]$e_{m}$, where this is the base object and each of $x_{i}$ are the formal argument in the method declration and $e_{m}$ is the body of the method m.

• –

if e is a value and $\exists e_{i}$ $1\leq i\leq p$, such that $e_{i}\rightarrow e_{i^{\prime}}$, then t $\rightarrow$ t’ with t’ := e.m($e_{1}$, $e_{2}$,… $e_{i-1}$, $e_{i^{\prime}}$…,$e_{p}$).

• –

if e $\rightarrow$ e’ then t $\rightarrow$ t’ with t’ := e’.m($e_{1}$, $e_{2}$,…, $e_{p}$).

• •

T-While - t := while [$\exists.\phi$] ($e_{1}:Bool$, $e_{2}$); stmt , this is a standard While case with case wise split for $e_{1}$ = true and false.

Theorem 7.3 (Preservation)

if $\Gamma$, $\Phi$ $\vdash$ t : $\tau$ and t $\rightarrow$ t’, then ($\Gamma^{\prime}$, $\Phi^{\prime}$) $\vdash$ t’ : $\tau^{\prime}$ and ($\Gamma^{\prime}$, $\Phi^{\prime}$) $\vdash$ $\tau^{\prime}$ type.

Proof

The proof is by the induction on the derivation of $(\Phi,\Gamma)\vdash t:\tau$ 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 $\nexists$ t’ such that t $\rightarrow$ t’ and thus the argument vacuously holds for these typing derivation rules.

• •

T-F-Ref , t := e.f : $\tau$ type, now by IH if e $\rightarrow$ e’ then t $\rightarrow$ t’, where t’ := e’.f and e’ is well typed. By T-F-Ref ($\exists\phi_{e},s_{e},\tau_{e}\ and\ \phi_{e^{\prime}},s_{e^{\prime}},\tau_{e^{\prime}}$), such that $\Gamma(e):=(\phi_{e},s_{e}).\tau_{e}$ and $\Gamma(e^{\prime}):=(\phi_{e^{\prime}},s_{e^{\prime}}).\tau_{e^{\prime}}$. Let sdecl $s_{e^{\prime}}$ = state $s_{e^{\prime}}$ case of $s_{x}$ {… $f:\tau_{f}$..}, thus the type of t’ := $\tau_{f}$.

• •

T-Update, t := e $\leftarrow$ e’ and $(\Phi,\Gamma\vdash)$ t : $\tau$, if e’ $\rightarrow$ e”, then t $\rightarrow$ t’ and t’ := e $\leftarrow$ e”. By IH if $(\Phi,\Gamma)\vdash$ e’ : $\tau^{\prime}$ then after e’ $\rightarrow$ e”, $(\Phi,\Gamma)\vdash$ e” : $\tau^{\prime\prime}$. Thus by T-update, $(\Phi,\Gamma\vdash)$ t’ : $\tau^{\prime\prime}$).

• •

T-match, t := match $e_{1}$ $\overline{\textnormal{case}e_{i}}$, $(\Phi,\Gamma)\vdash$ t : $\tau_{1}\rightarrow\tau_{u}$. There are two possible ways of reduction of t $\rightarrow$ t’-

• –

If $e_{1}\rightarrow e_{1^{\prime}}$, then t $\rightarrow$ t’, such that t’ := match $e_{1^{\prime}}$ $\overline{\textnormal{case}e_{i}}$. By IH if $(\Phi,\Gamma)\vdash e_{1}:\tau_{1}$ then $(\Phi,\Gamma)\vdash e_{1^{\prime}}:\tau_{1}^{\prime}$. By T-match, $(\Phi,\Gamma)\vdash t^{\prime}:(\tau_{1}^{\prime}\rightarrow\tau_{u})$.

• –

If for some $e_{i}$, $e_{i}\rightarrow e_{i^{\prime}}$ then t $\rightarrow$ t’, such that t’ := match $e_{1}$ $\overline{\textnormal{case}\ e_{i-1}}\ casee_{i^{\prime}}\ \overline{\textnormal{case}\ e_{i+1}}$. By IH, if $(\Phi,\Gamma)\vdash e_{i}:tau_{i}$ then $(\Phi,\Gamma)\vdash e_{i^{\prime}}:\tau_{i}^{\prime}$. By T-match, let $\tau_{u}^{\prime}$ = $\bigcup\tau_{1}...\tau_{i-1}\tau_{i^{\prime}}..\tau_{k}$ then $(\Phi,\Gamma)\vdash t^{\prime}:(\tau_{1}\rightarrow\tau_{u}^{\prime})$.

• •

T-let, t := let x = $e_{1}$ in e. There are two distinct possibilities of reduction of t $\rightarrow$ t’-

• –

If $e_{1}\rightarrow e_{1^{\prime}}$, by IH $(\Phi,\Gamma)\vdash$ $e_{1}^{\prime}:\tau_{1}^{\prime}$. Let $(\Phi,\Gamma,x:\tau_{1}^{\prime},e_{1}^{\prime}:\tau_{1}^{\prime})\vdash$ e : $\tau^{\prime}$, then t’ := let x = $e_{1}^{\prime}$ in e and $(\Phi,\Gamma)\vdash$ t’ : $\tau^{\prime}$.

• –

If e $\rightarrow$ e’, by IH $(\Phi,\Gamma)\vdash e^{\prime}:\tau^{\prime}$. thus for t $\rightarrow$ t’, $(\Phi,\Gamma)\vdash$ t’ : $\tau^{\prime}$.

• •

T-mcall, t := e.m($e_{1},e_{2},...,e_{p}$). There are two distinct possibilities of reduction of t $\rightarrow$ t’-

• –

e.m(…) $\rightarrow$ e’.m(…), if e $\rightarrow$ e’. By IH, let $(\Phi,\Gamma)\vdash$ e’ : $\tau_{b}^{\prime}$. By T-mcall, let $((\Phi\wedge(\bigwedge_{i}\Phi_{i})(\Gamma,e^{\prime}:\tau_{b}^{\prime},\overline{e_{i}:\tau_{i})})\vdash e_{m}:T_{r}^{\prime})$ then t’ : $T_{r}^{\prime}$.

• –

e.m(…,$e_{k}$,…,$e_{p}$) $\rightarrow$ e.m(…,$e_{k}^{\prime}$,…,$e_{p}$) for some $k\in[1,p]$ if $e_{k}\rightarrow e_{k}^{\prime}$. By IH $(\Phi,\Gamma)\vdash$ $e_{k}^{\prime}$ : $\tau_{k}^{\prime}$. By T-mcall, let $((\Phi\wedge(\bigwedge_{i}\Phi_{i})(\Gamma,e:\tau_{b},\forall i\in\{[1,p]\setminus k\}\overline{e_{i}:\tau_{i})},e_{k}^{\prime}:\tau_{k}^{\prime})\vdash e_{m}:T_{r}^{\prime})$, then t’ : $T_{r}^{\prime}$.

• •

T-while, while [$\exists.\phi$] ($e_{1}$) {e}. Again two distinct possible way of reduction of t $\rightarrow$ t’-

• –

If $e_{1}\rightarrow e_{1}^{\prime}$, by T-while $e_{1}^{\prime}:bool$, and let $(\Phi_{1}\wedge(e_{1}^{\prime}==true),(\Gamma,e_{1}^{\prime}:bool))\vdash e:(\Phi_{2},\tau^{\prime})\ \ \Phi_{2}\vDash\exists.\phi$, then t’ : $\tau^{\prime}$.

• –

If e $\rightarrow$ e’, By IH $(\Phi_{1}\wedge(e_{1}==true),(\Gamma,e_{1}:bool))\vdash e^{\prime}:(\Phi_{2},\tau^{\prime})\ \ \Phi_{2}\vDash\exists.\phi$, then t’ : $\tau^{\prime}$.

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 $(\Phi,\Gamma)\vdash t:(\Phi^{\prime},\tau)$ in our typestate system, $\exists.\psi\in PresburgerArithmeticFormula$, such that $(\Phi,\Gamma)\vdash t:(\Phi^{\prime},\tau)$ holds iff $\psi$ 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 $\psi(\tau)$ defines the presburger formula for $\tau$. We consider here only the base types and other complex types and show the PAF $\psi$ for each of these.

• •

Base case : $\forall$ primary type $\tau\in\{void,int,bool,String\}$, $\psi(\tau)$ = $\phi_{\tau}$ = $\exists x_{\tau}.x_{\tau}\neq 0$.

• •

Case :: $\tau=S$, let $x_{s}$ define a variable for the state S, then the formula $\psi(\tau)=x_{s}\neq 0$.

• •

Case :: $\tau_{i}<:\tau_{j}$, by IH let $\psi(\tau_{i})$ = $\phi_{\tau_{i}}$ and $\psi(\tau_{j})$ = $\phi_{\tau_{j}}$, then $\psi(\tau_{i}<:\tau_{j})$ = $\phi_{\tau_{i}}\vDash\phi_{\tau_{j}}$.

• •

Case :: $\tau_{i}=\tau_{j}$, by IH let $\psi(\tau_{i})$ = $\phi_{\tau_{i}}$ and $\psi(\tau_{j})$ = $\phi_{\tau_{j}}$, then $\psi(\tau_{i}=\tau_{j})$ = $\psi(\tau_{i}<:\tau_{j})\wedge\psi(\tau_{j}<:\tau_{i})$ .

• •

Case :: $\tau_{i}\rightarrow\tau_{j}$, By expression typing rules, $\exists.mdecl=\tau_{j}m(\tau_{i}\ a_{i})\{...e_{b}:\tau_{b}...\}$. By IH let $\psi(\tau_{i})$ = $\phi_{\tau_{i}}$ and $\psi(\tau_{j})$ = $\phi_{\tau_{j}}$ and $\psi(\tau_{b})=\phi_{\tau_{b}}$, then $\psi(\tau_{i}\rightarrow\tau_{j})$ = $\psi(\psi((\tau_{i})\wedge\psi(\tau_{b}))<:\psi(\tau_{j}))$.

• •

Case :: $\tau_{i}\gg\tau_{j}$, the case is similar to the $\tau_{i}\rightarrow\tau_{j}$ 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 $s-9<b<s+9$, its late iff $b\in[s-9,s-1]$, its early iff $b\geq s+9$ finally, when $b=s+1$, the train is on time again.

One property of interest to avoid collisions is- $\forall time,\mid b-s\mid\leq 20$, which could not be enforced using regular typestate. We present a counter machine for the train speed control protocol in appendix section figure  15.