text:
Hybrid Types, Invariants, and Refinements For Imperative Objects
- Silvia Harrell
- 2 years ago
- Views:
1 Hybrid Types, Invariants, and Refinements For Imperative Objects Cormac Flanagan Department of Computer Science University of California, Santa Cruz Stephen N. Freund Department of Computer Science Williams College Aaron Tomb Department of Computer Science University of California, Santa Cruz Abstract To control the complexity of large object-oriented systems, objects should communicate via precisely-specified interfaces. Static type checking catches many interface violations early in the development cycle, but decidability limitations preclude checking all desired properties statically. In contrast, dynamic checking supports expressive specifications but may miss errors on execution paths that are not tested. We present a hybrid approach for checking precise object specifications that reasons statically, where possible, but also dynamically, when necessary. This hybrid approach supports a rich specification language with features such as object invariants and refinement types. 1. Introduction The construction and validation of large software systems is extremely challenging. To control the complexity of such systems, they are ideally constructed as a collection of objects that cooperate via precisely-specified interfaces. These interface specifications then enable individual objects to change and evolve without the need to understand the entire system. Thus, a key challenge in the construction of any objectoriented system is to precisely specify object interfaces, and to verify (to the degree possible) that object implementations respect these interfaces. Types can naturally describe some aspects of object interfaces. An advantage of these type specifications is that static type checking can then catch many errors at compile time, when they are cheaper to fix. However, static type checking is possible only for certain kinds of specifications, and extending the type language to support expressive specifications, such as arbitrary method preconditions and postconditions, results in a type system that is not statically decidable. Hence, traditional object type systems cannot express many useful interface specifications, such as: The method getcount returns a positive number. The field i of an object is a valid index into the array in the field a. This object contains a sorted list. The method draw expects a Point object that is within a specified rectangle. Other static checkers suffer from similar limitations. For example, ESC/Java [14] may reject valid programs due to the incompleteness of its theorem prover. Presented at the FOOL/WOOD Workshop, January, In contrast, precise object specifications are straightforward to check dynamically, either via assert statements [37] or via specialized contract languages [29, 11, 24, 16, 20, 26, 34, 21]. However, dynamic checking imposes a certain performance overhead. More seriously, dynamic checking only detects errors on code paths and data values of actual executions. Thus, dynamic checking may not catch errors until very late in the development cycle, or possibly postdeployment, when they are significantly more expensive to fix. In summary, decidable static type checkers provide complete checking of limited specifications, while dynamic approaches provide limited coverage of expressive specifications. In this paper, we explore a hybrid approach to checking expressive object specifications that combines the advantages of these prior purely-static and purely-dynamic approaches. In a nutshell, hybrid type checking involves: 1. embracing expressive type languages that can document precise object interfaces, but which are therefore statically undecidable; 2. leveraging static type checking to detect as many errors as possible at compile time; and 3. leveraging dynamic checking to check any remaining (not statically verified) correctness properties at run time. Our specification language extends an Abadi-Cardellistyle type system [1] with refinement types and object invariants. A refinement type defines a subset or refinement of an existing type [28, 15, 8, 43, 42]. For example, the refinement type {x : Int x > 0} denotes the set of positive integers. For expressiveness, our type system requires only that refinement predicates be pure; that is, refinement predicates are arbitrary program expressions that do not access mutable data. Each object type also has an associated predicate, called an object invariant, which must hold on all objects of that type. We formalize the semantics of this expressive specification language using a type system that is sound but necessarily undecidable. To enable useful checking, we then present a hybrid type checking algorithm with the following desirable features: 1. The hybrid type checker statically rejects as many illtyped programs as possible. 2. Due to decidability limitations, the hybrid type checker may statically accept some subtly ill-typed programs, but it will insert sufficient dynamic casts to guarantee that their specifications are never violated. Any attempted specification violation is thus either caught statically
2 (where possible) or via dynamic checks (where necessary). 3. The output of the hybrid type checker is always a welltyped program (and so, for example, type-directed optimizations are applicable). In previous work, we explored this hybrid strategy in the simpler context of the pure functional lambda-calculus [12, 18]. To help verify large object-oriented systems, this paper extends these earlier ideas to a more interesting imperative language that supports objects (with both final and mutable methods, and imperative method update) and expressive object specifications (with object subtyping, refinement types, and object invariants). This initial work studies hybrid type checking in the context of an idealized object language, but we hope that this work will serve as a foundation for exploring more complex object languages and type systems. Our long term goal is to apply hybrid type checking to realistic objectoriented programming languages, such as Java [17], C# [10], or Objective CAML [35]. The presentation of our results proceeds as follows. The next section informally describes our object language and type system. Section 3 applies this type language to document some precise specifications. Section 4 and 5 formally describe the operational semantics and (undecidable) type system for this language. Section 6 presents our hybrid type checking algorithm, and Section 7 states the key correctness properties of our type system and compilation algorithm. Section 8 discusses related work, and Section 9 concludes. 2. The Hoop Language We present our approach to hybrid checking of expressive object specifications in terms of Hoop, an idealized hybrid object-oriented programming language based on the calculi of Abadi and Cardelli [1]. The syntax of this language is shown in Figure Types We begin with an overview of the type language, since it contains a number of features that are unusual in object type systems, such as dependent types, refinement types, and object invariants. A base type B is either Bool, Int, or Unit. Since these base types are fairly coarse and cannot, for example, express integer subranges, we introduce refinement types such as {x : Int x > 0}, which denotes the set of positive integers. More generally, the refinement type {x : B t} denotes the set of values c of type B that satisfy the boolean predicate t, i.e., for which the term t[x := c] evaluates to true. We use a base type B as an abbreviation for the refinement type {x:b true}. Our refinement types are inspired by prior work on decidable refinement type systems [28, 15, 8, 43, 42] but are more expressive, which causes type checking to be undecidable. In particular, subtyping between two refinement types {x:b t 1} and {x:b t 2} reduces to checking implication between the corresponding (arbitrary) refinement predicates, which is clearly undecidable. These decidability difficulties are circumvented by our hybrid type checking algorithm. An object type in our language has the form x:[l i : f i p i (y :T i T i ) i 1..n ].t This type denotes an object containing n methods with distinct names l 1..n. (As usual, fields can be encoded as Figure 1: Syntax s, t, u ::= Terms: x variable d object v value t.l(s) select t.l ς(x, y)u update T t cast let x = s in t as T binding d ::= x.[l i(y) = t i i 1..n ] as T Objects: object v, w ::= Values: c constant a object address a view T object view S, T, U ::= Types: {x:b t} base refinement type x:[l i : f i p i M i 1..n i ].t object type M, N ::= Method Types: y :T i T i method type B ::= Unit Bool Int f ::= final mutable p ::= pure impure Base types: Final modifiers: Purity modifiers: methods.) Each method l i has the dependent type (y :T i T i ), meaning that it takes an argument of type T i, and returns a result of type T i, where the formal parameter y may occur free in T i. We abbreviate (y : T i T i ) by (T i T i ) if y does not occur free in T i. Since our type system contains dependent types that may refer to variables, each object type includes a binding for the self-reference variable x (often called this) that may be mentioned in method types. Each method l i also has two method qualifiers f i and p i. The method qualifier f i {final, mutable} indicates whether the corresponding method can be updated. Object subtyping is invariant on mutable methods, and covariant on immutable (or final) methods. The method qualifier p i {pure, impure} indicates whether the method l i is pure. Specifically, an expression is pure if its evaluation never accesses (i.e., invokes or updates) a mutable method. Purity qualifiers are ordered by pure impure, since it is safe to consider a pure method to be impure. Each object type includes an object invariant t, which is a boolean predicate over the self-reference variable x. This object invariant is guaranteed to hold for any object of this type, and so cannot evaluate to false. To ensure that this guarantee holds in the presence of method updates, we require that every object invariant be pure. Similarly, refinement predicates must also be pure.
3 2.2 Terms Hoop source terms include variables, constants, objects, method invocation and update, casts, and let-expressions. An object d has the form x.[l i(y) = t i i 1..n ] as T and consists of a collection of methods l 1..n with corresponding method bodies t 1..n, where x and y provide bindings for the self-reference variable and the formal parameter, respectively. Each object is annotated with an explicit type T. Constants in Hoop include boolean and integer constants, as well as operations such as +,, and, and not. Although our examples use infix notation for primitive operations, Hoop internally represents these primitive operations as method invocations. A cast T t dynamically converts (where possible) the value produced by t to type T, or else fails. For technical reasons, let bindings include an explicit type annotation. Hoop also includes object addresses a and object views (a view T ). These constructs are used to formalize the operational semantics of the language, and should not appear in source programs. 3. Examples In this section, we illustrate our type language and hybrid type checking through several informal examples. For readability, we omit final and pure modifiers and assume methods are immutable and pure unless specified otherwise. 3.1 Refinement Types We first introduce some useful refinements of Int: Pos {z :Int z > 0} Nat {z :Int z 0} Since (z > 0) (z 0), the expected subtype relation Pos <: Nat holds. Similarly, since (z 0) true, we also have that Nat <: Int. Subtyping between refinement types is undecidable in general, and therefore so is type checking. For example, consider the method update: p.m ς(x, y)t where x and y provide bindings for the self-reference variable and formal parameter, respectively. Suppose the mutable method p.m has type Int Nat, and that the term t has type {z : Int z = y 2 }. To check if this method update is well-typed, the compiler needs to decide the subtype relation {z :Int z = y 2 } <: Nat which in turn reduces to deciding the validity of the implication: (z = y 2 ) (z 0) If the compiler can prove this implication, then t has type Nat (via subsumption), and so the method update is welltyped. Conversely, if the compiler can refute this implication, then t does not have type Nat, and the compiler can reject the program as ill-typed. (In this case, however, the implication is valid and so cannot be refuted.) Due to the expressiveness of the Hoop type language, the compiler may encounter situations where its algorithms can neither prove nor refute such implications, and so the compiler cannot decide whether or not expressions are welltyped. A key design question is how the compiler should handle such situations. Optimistically accepting such programs means that type specifications cannot be trusted, since they may be violated at run time, which is clearly undesirable. Pessimistically rejecting such programs would cause the compiler to reject some well-typed programs, which seems too brittle for use in practice, since it would be difficult to predict which programs the compiler would accept. Hybrid type checking handles such situations by provisionally accepting the program but inserting a cast that dynamically enforces the specification of p.m, yielding the compiled code: p.m ς(x, y)( Nat t) This compiled code is well-typed, and it dynamically ensures that the specification of p.m is never violated, i.e., the method p.m only returns natural numbers. This example illustrates how hybrid type checking enforces precise specifications, such as Int Nat, even if those specifications cannot be always verified statically. In comparison, a static type checker may be able to enforce only weaker specifications, such as Int Int. 3.2 Pairs We next define an object pair containing two integers and a method that computes their sum. We assign pair a conventional type Pair: pair p.[a = 3, b = 5, sum( ) = p.a + p.b] as Pair Pair p:[a : Int, b : Int, sum : Unit Int] Although Hoop does not directly support fields, we may encode a field of type T as a method of type Unit T. We abbreviate such a field type to simply T for readability. For sum, we use the parameter name to indicate that this value is not used in the method body. Alternatively, we could use refinement types to specify that the second component of the pair is not less than the first: 2 OrderedPair p: 4 a : Int, 3 b : {z :Int z p.a}, 5 sum : Unit Int This type specifies that if the method b terminates, it must return an integer greater than p.a. Note that the predicate z p.a must be pure. Our type system ensures that pure expressions cannot access mutable data. Without this restriction, a program could use subtyping to hide the field b and then break the predicate on b by modifying a. We permit covariant subtyping of immutable fields, meaning that OrderedPair <: Pair An alternative definition of OrderedPair uses an object invariant to express the ordering relation between a and b: OrderedPair 2 p: 4 a : Int, b : Int, sum : Unit Int 3 5.(p.a p.b) For any object p of this type OrderedPair, the object invariant (p.a p.b) must never return false; it can only return true, or it may diverge. 1 In particular, the method calls p.a and p.b can diverge without violating this object invariant. 1 Allowing object invariants to diverge avoids the complexity of reasoning about termination in the type system
4 We require that the invariant of a subtype imply the invariant of its supertype. For example, since the implication (p.a p.b) true holds, we have that: OrderedPair <: Pair We check invariant implication in a context in which we know the precise type of the self-reference variable. Thus, since for all p of type OrderedPair, the predicate (p.a p.b) never evaluates to false, we can conclude that true (p.a p.b), and hence that: OrderedPair <: OrderedPair Thus, subtyping allows us to move information from method specifications to the object invariant. One interesting difference between object invariants and precise method specifications is that the latter can specify the behavior of mutable methods. For example, the following type allows the method b to be updated with any integer that is not less than a: MutableOrderedPair 2 p: 4 a : Int, 3 b : mutable impure {z :Int z p.a}, 5 sum : impure Unit Int 3.3 Geometric Objects As a final example, consider the following types for points, rectangles, and squares: Point p:[x : Int, y : Int] Rectangle r :[b : Point, w : Nat, h : Nat] Square r :[b : Point, w : Nat, h : Nat].(r.w = r.h) Clearly, Square <: Rectangle. The following subtype of Point allows us to describe points must lie within a given Rectangle r: PtInRect(r) p:[x : Int, y : Int]. «(r.b.x) p.x (r.b.x + r.w) (r.b.y) p.y (r.b.y + r.h) We can also specify a type of mutable points, and a subtype of mutable points that must stay within a given rectangle:» x : mutable impure Int, MutablePoint p: y : mutable impure Int MutablePtInRect(r)» x : mut. imp. {z :Int r.b.x z r.b.x + r.w}, p: y : mut. imp. {z :Int r.b.y z r.b.y + r.h} The compiler will ensure that all updates to an object of type MutablePtInRect(r) are within the specified bounds, either via static reasoning, where possible, or else via implicit dynamic checks, if necessary. We can also specify more general relationships, such as the type of all points occurring within a particular Shape, where Shape has subtypes Rectangle and Circle, all of which implement a contains method: Shape p:[contains : Point Bool] Rectangle p:[contains : Point Bool,...] Circle p:[contains : Point Bool,...] The following type then characterizes points that must lie within a particular Shape: PtInShape(s) p:[x : Int, y : Int].(s.contains(p)) 4. Hoop Operational Semantics We formalize the run-time behavior of Hoop programs using the small-step operational semantics shown in Figure 2. Evaluation is performed inside evaluation contexts, which are defined by the grammar: E ::= E.l(t) v.l(e) E.l ς(x, y)u T E let x = E in t as T A store σ maps object addresses a to objects d, and we use to denote the empty store. A state (σ, t) is a pair of a store and a term. The relation (σ, t) (σ, t ) performs a single evaluation step, and the relation is the transitive closure of. The first five evaluation rules are fairly straightforward. The rule [E-Obj] adds a new object to the store at a fresh address. The rule [E-Sel-Obj] for a method invocation a.l j(v) extracts the method body t j from the object at address a, and replaces the self-reference variable x and the formal parameter y with the object address a and the argument v, respectively. The rule [E-Upd] for a method update a.l j ς(x, y)u replaces the method l j in the object at address a. We use α-renaming to implicitly match the self-reference and parameter variables of the original and new methods. The rule [E-Let] for (let x = v in t as T ) simply replaces x by v in t. Constants include both basic constants, such as true and 3, and primitive operations, such as not and +. Primitive operations are actually objects with an apply method that provides the required functionality. The prefix and infix syntax for primitive operations shown in the earlier examples is actually desugared into invocations of apply methods, as follows: not true not.apply(true) apply( (3 : Int, 4 : Int) ) The desugaring for + uses the following notations for creating objects representing pair of values: S T x:[fst : S, snd : T ] (v 1 : S, v 2 : T ) x.[fst = v 1, snd = v 2] as (S T ) The rule [E-Const] evaluates a method invocation c.l(v) on a primitive operation c, and relies on the meaning function [ ] to define the behavior of primitive operations. Specifically, [c](l, v, σ) returns the result of invoking the method l of the primitive operation c on the argument v in store σ. For example, if σ(a) contains the pair (3 : Int, 4 : Int), we have: [not](apply, true, σ) = false [+](apply, a, σ) = 7 [ ](apply, a, σ) = true [and ](apply, a, σ) = undefined The rule [E-CastBase] casts a constant c to refinement type {x : B t} by checking that the predicate t holds on c, i.e., that t[x := c] evaluates to true. If t[x := c] returns false or diverges, then the cast is said to fail. Casts on object types are more complicated, since we need to check that every method of the resulting casted object returns a value of the appropriate type for all possible argument values. This check is performed in a lazy manner
5 Figure 2: Evaluation Rules Evaluation (σ, t) (σ, t ) In the following rules, we assume: d = x.[l i(y) = t i 1..n i ] as S S = x:[l i : f i q i (y :S i S i) i 1..n ].s T = x:[l i : f i p i (y :T i T i ) i 1..m ].t T = x:[l i : f i p i (y :T i T i ) i 1..m ] a dom(σ) (σ, E[d]) (σ[a := d], E[a]) σ(a) = d (σ, E[a.l j(v)]) (σ, E[t j[x := a, y := v]]) σ(a) = d d = x.[l i(y) = t i 1..j 1 i, l j(y) = u, l i(y) = t i j+1..n i ] as S (σ, E[a.l j ς(x, y)u]) (σ[a := d ], E[unit]) (σ, E[let x = v in t as T ]) (σ, E[t[x := v]]) [c](l, v, σ) = v (σ, E[c.l(v)]) (σ, E[v ]) (σ, t[x := c]) (σ, true) (σ, E[ {x:b t} c]) (σ, E[c]) σ(a) = d m n q i p i i 1..m (σ, t [x := (a view T )]) (σ, true) (σ, E[ T a]) (σ, E[a view T ]) σ(a) = d v = S j[x := a] v R = T j[x := (a view T ), y := v] (σ, E[(a view T ).l j(v)]) (σ, E[ R (a.l j(v ))]) σ(a) = d u = ( S j (u[y := T j y][x := (a view T )])) (σ, E[(a view T ).l j ς(x, y)u]) (σ, E[a.l j ς(x, y)u ]) (σ, E[ T (a view S)]) (σ, E[ T a]) [E-Obj] [E-Sel-Obj] [E-Upd-Obj] [E-Let] [E-Const] [E-Cast-Base] [E-Cast-Obj] [E-Sel-View] [E-Upd-View] [E-Cast-View] via object views. An object view (a view T ) is a wrapper that ensures that the object σ(a) behaves according to the specification of type T. Views are introduced by the rule [E-Cast-Obj], which evaluates the cast T a to the view (a view T ). In addition, this rule checks that the object σ(a) has all the methods mentioned in T (with compatible modifiers), and that the object invariant of T holds on σ(a). We define special evaluation rules for method invocation and update on views. These rules lazily enforce typing restrictions on method parameters and results by performing appropriate checks on method invocations and updates. The rule [E-Sel-View] for a view invocation (a view T ).l j(v) retrieves the type S of a, which may be quite different from the view type T : S = x:[l i : f i q i (y :S i S i) i 1..n ].s T = x:[l i : f i p i (y :T i T i ) i 1..m ].t The rule reduces the view invocation (a view T ).l j(v) to the following method invocation, which contains two additional casts to ensure type safety: T j[x := (a view T ), y := v] (a.l j( S j[x := a] v)) The cast S j[x := a] v transforms the argument v of type T j to a value of the expected argument type S j, where self-reference variable x is replaced by object s address a. The cast T j[x := (a view T ), y := v] (...) transforms the method result into the expected type T j, where self-reference variable x and formal parameter y are replaced by original view (a view T ) and original argument v, respectively. These two casts ensure that method invocations on object views preserve type safety. To illustrate this guarantee, suppose: σ(a) = x.[fact(y) =...] as Fact Fact x:[fact : Nat Nat] BadFact x:[fact : Int Nat] and consider the term ( BadFact a).fact( 3), which attempts to use the BadFact view to circumvent the Fact specification of the object σ(a). This term evaluates to Nat (a.fact( Nat 3)), at which point the cast ( Nat 3) fails. Thus, the casts inserted by [E-Sel-View] enforce the specification of the fact method, which states that fact should be applied only to natural numbers. The rule [E-Upd-View] reduces a view update to a normal method update (a view T ).l j ς(x, y)u a.l j ς(x, y)u where u is the following modified version of u with additional casts: u = ( S j (u[y := T j y][x := (a view T )])) Here, the formal parameter y in u is replaced with T j y, which is guaranteed to be of the appropriate type T j, even though y itself may not be. Similarly, the self-reference variable x is replaced with the view (a view T ), which is of the expected type T, even though a may not be. 2 Finally, the result of u is cast to type S j, which is the return type expected by (non-view) invocations of a.l j. The rule [E-Cast-View] evaluates T (a view S) to T a; thus, the original view is discarded when cast to a different view. In summary, casts allow the program to claim that a value of one type can be safely considered to be of another type, and the operational semantics performs sufficient runtime checking to detect if this claim is ever violated. This 2 The alternative of substituting ( T x) for x would require redundant re-evaluation of T s object invariant.
6 ability to perform dynamic casts is crucial for enabling our hybrid type checking algorithm to convert particularly difficult static checks into dynamic checks, when necessary. 5. The Hoop Type System We next present the (undecidable) type system for the Hoop language as the collection of the type judgments and rules shown in Figures 3 and 4. Type environments are a sequence of variable-type bindings, and we assume that the variables bound in an environment are distinct. E ::= E, x : T The judgment E t : T & p states that the term t has type T and purity p in environment E. This judgment is defined by the following rules: The rule [T-Var] states that variable accesses are always pure, since variables are immutable. The rule [T-Obj] deals with object creation, and checks that each method has the appropriate result type and purity. In addition, a mutable method is considered impure, since any call to that method must be impure. Newlycreated objects must have the trivial invariant true. A stronger invariant can later be added via subtyping or casting. The rule [T-Let] for let x = t 1 in t 2 as T requires that the type T of t 2 must be well-formed in the environment without x, in order to prevent x from escaping its scope. The rule [T-Sel] for a method invocation t.l j(u) checks that the method l j has type y : T j T j, and that the argument u has type T j[x := t]. The type of the method call is then T j[x := t, y := u], where the self-reference variable x and the formal parameter y are replaced by the object t and the actual parameter u, respectively. Since the terms t and u may appear in the resulting type, these terms must be pure. Note that if one of these terms, say t, is not pure, the method call t.l j(u) can be refactored into (let x = t in x.l j(u) as R), provided the explicit result type R does not mention x. The rule [T-Upd] for a method update checks that the updated method is mutable and that the new method body has the appropriate type and purity. The rule [T-Const] assigns the type ty(c) to each constant c. Basic constants have precise refinement types, such as: true : {b:bool b} false : {b:bool not b} n : {m:int m = n} Primitive operations are assigned object types that precisely characterize their behavior. For example, the following type for + states that the method +.apply takes two integer arguments, which are passed in the fst and snd fields of the pair object y, and that the method result is an integer r that is equal to (y.fst + y.snd).» «y : (Int Int) + : x: apply : {r :Int r = y.fst + y.snd}» y : (Bool Bool) : x: apply :» {r :Bool r (y.fst «y.snd)} y : Bool not : x: apply :» {r :Bool r not y} y : (Int Int) = : x: apply : {r :Bool r (y.fst = y.snd)} ««Figure 3: Type Rules Type Rules for Terms (x : T ) E E x : T & pure E T T = x:[l i : f i p i (y :T i T i ) i 1..n ] f i = mutable p i = impure i 1..n E, x : T, y : T i s i : T i & p i i 1..n E (x.[l i(y) = s i 1..n i ] as T ) : T & pure E t 1 : S & p 1 E, x : S t 2 : T & p 2 E T E let x = t 1 in t 2 as T : T & (p 1 p 2) E t : T & pure T = x:[l i : f i p i (y :T i T i ) i 1..n ].s E u : T j[x := t] & pure j 1..n E t.l j(u) : T j[x := t, y := u] & p j E t : T & p T = x:[l i : f i p i (y :T i T i ) i 1..n ].s j 1..n f j = mutable E, x : T, y : T j u : T j & p j E t.l j ς(x, y)u : Unit & impure E c : ty(c) & pure E t : S & p E T E T t : T & p E t : S & q E S <: T q p E t : T & p Type Rules for Types E, x : B t : Bool & pure E {x:b t} T = x:[l i : f i p i (y :T i T i ) i 1..n ].t S k = x:[l i : f i p i (y :T i T i ) i 1..k ] E, x : S j 1 T j j 1..n E, x : S j 1, y : T j T j j 1..n E, x : S n t : Bool & pure E T E t : T & p [T-Var] [T-Obj] [T-Let] [T-Sel] [T-Upd] [T-Const] [T-Cast] [T-Sub] E T [T-Base] [T-ObjTy] The apparent circularity where the type of + is defined in terms of + itself does not cause any technical difficulties in our development, since the meaning of the refinement predicate is defined in terms of the operational semantics, and hence in terms of the meaning function [+]. The rule [T-Cast] allows a term of inferred type S to be cast to any other (well-formed) type T. Note that this cast may fail at run time.
7 Figure 4: Subtyping Subtyping E, x : B s t E {x:b s} <: {x:b t} S = x:[l i : f i q i M i 1..n i ].s T = x:[l i : f i p i N i 1..m i ].t m n q i p i i 1..m f i = final E, x : S M i <: N i i 1..m f i = mutable E, x : S M i = N i i 1..m E, x : S s t E S <: T Method Subtyping E T i <: S i E, y : T i S i <: T i E (y :S i S i) <: (y :T i T i ) Method Equality E M <: N E N <: M E M = N Implication θ. (E = θ (, θ(t)) (σ, false)) (, θ(s)) (σ, false) E s t Consistent Substitutions E S <: T [S-Base] [S-Obj] E M <: N [M-Sub] E M = N [M-Equal] E s t [Imp] E = θ The rule [T-ObjTy] states that object invariants must have type Bool and be pure, and that each method type can only refer to methods declared earlier in the object. The most interesting part of our type system concerns the rules that define the subtyping judgment E S <: T in Figure 4. This subtyping judgment is complicated by the expressiveness of refinement predicates and object invariants, and it is defined in terms of the implication judgment E s t. Essentially, this implication judgment holds if whenever the term t evaluates to false, the term s must also evaluate to false. More formally, we define a substitution θ (from variables to terms) to be consistent with an environment E if θ maps variables to terms in a manner that is consistent with the type bindings in E. The implication judgment E s t then holds if for all substitutions θ consistent with E such that θ(t) evaluates to false, it follows that θ(s) also evaluates to false. Subtyping between refinement types then reduces to an implication judgment between the refinement predicates, via the rule [S-Base]. Subtyping between two object types S and T is covariant on immutable methods and invariant on mutable methods. Subtyping also involves checking implication between object invariants. Note that this implication check is performed in an environment where the selfreference variable has type S. This binding allows subtyping to refactor type information from method types to the object invariant. For example, suppose: S = x:[m : {z :Int z 0}] T = x:[m : Int ].(x.m 0) Clearly, if the variable x has type S, then the object invariant (x.m 0) returns true, or else diverges. Hence: x : S true (x.m 0) and so S <: T. This subtyping judgment has the effect of refactoring information about the method m from the method type to the object invariant. = ɛ t : T & pure E[x := t] = [y i := t i i 1..n ] x : T, E = [x := t, y i := t i i 1..n ] Well-formed environments E E T E, x : T [Sub-Empty] [Sub-Ext] E [WE-Empty] [WE-Ext] The rule [T-Sub] allows the inferred type S of a term to be weakened to any super type T. The judgment E T checks that the type T is well-formed in environment E. The rule [T-Base] states that refinement predicates must have type Bool and be pure. 6. Hybrid Type Checking Given that type checking is undecidable, we now present a decidable compilation strategy for Hoop programs. This compilation strategy ensures (by inserting dynamic checks, if necessary) that specifications can never be violated at run time, and it statically rejects clearly ill-typed programs. The compilation strategy relies on an algorithm to conservatively approximate the logical implication judgment E s t. The result of this algorithm is denoted as: E a alg s t where the mode a {,,?} indicates whether or not the algorithm is successful at verifying or refuting the given implication. In particular, E alg s t means the algorithm successfully determines that E s t. E alg s t means the algorithm determines that the implication does not hold, i.e., E s t. E? alg s t means the algorithm fails to either prove or disprove that E s t. However, we do not require that the algorithm be complete. For example, the trivial algorithm that always returns? satisfies our requirements, although it precludes performing any interesting reasoning in the compiler.
8 Figure 5: Algorithmic Subtyping Figure 6: Compilation Rules Algorithmic Subtyping E a alg S <: T Compilation of Terms E s t : T & p E, x : B a alg s t E a alg {x:b s} <: {x:b t} [AS-Base] (x : T ) E E x x : T & pure [C-Var] f i = final S = x:[l i : f i q i M i i 1..n ].s T = x:[l i : f i p i N i i 1..m ].t m n q i p i i 1..m E, x : S a i alg Mi <: Ni f i = mutable E, x : S a i alg Mi = Ni E, x : S a alg s t a = a a 1... a m E a alg S <: T Algorithmic Method Subtyping i 1..m i 1..m E a alg T i <: S i E, y : T i a alg S i <: T i E (a a ) alg (y :S i S i) <: (y :T i T i ) Algorithmic Method Equality [AS-Obj] E a alg M <: N [AM-Sub] E a alg M = N E S T T = x:[l i : f i p i (y :T i T i ) i 1..n ] f i = mutable p i = impure i 1..n E, x : T, y : T i s i t i T i & p i i 1..n E (x.[l i(y) = s i 1..n i ] as S) (x.[l i(y) = t i 1..n i ] as T ) : T & pure E s 1 t 1 : T & pure T = x:[l i : f i p i (y :T i T i ) i 1..n ].t E s 2 t 2 T j[x := t] & pure j 1..n E s 1.l j(s 2) t 1.l j(t 2) : T j[x := t 1, y := t 2] & p j E s t : T & p T = x:[l i : f i p i (y :T i T i ) i 1..n ].t j 1..n f j = mutable E, x : T, y : T i u u T j & p j E (s.l j ς(x, y)u) (t.l j ς(x, y)u ) : Unit & impure [C-Obj] [C-Sel] [C-Upd] E a alg M <: N E a alg N <: M E (a a ) alg M = N [AM-Equal] E c c : ty(c) & pure [C-Const] Figure 5 defines algorithmic subtyping and algorithmic type equality in terms of this implication algorithm. These rules closely match the corresponding rules in the type system. For example, algorithmic subtyping for base types directly reduces to an algorithmic implication test via [AS-Base]. For subtyping between object types, the rule [AS-Obj] uses the rules [AM-Sub] and [AM-Equal] to ensure the appropriate relationship between corresponding method types, and uses the implication algorithm to check implication of object invariants. As with algorithmic implication, algorithmic subtyping may not always yield a definitive answer. If all sub-tests succeed (or at least one sub-test fails) then the algorithm can conclude with certainty that subtyping does (or does not) hold. In other situations, the result of the whole test is uncertain. We use the 3-valued conjunction operator to compute the result of a subtype test based on the results of its subtests:????? We now define the hybrid compilation judgment E s t : T & p which compiles the term s into the term t, which has type T and purity p. The compilation rules type check the program s and insert additional type casts to compensate for indefinite answers returned by the subtyping algorithm, yielding the compiled program t. Successful compilation does not guarantee that the source program s is well-typed. However, E s t : U & p E S T E S s T t : T & p E s 1 t 1 : U & p 1 E S T E, x : U s 2 t 2 T & p 2 E (let x = s 1 in s 2 as S) (let x = t 1 in t 2 as T ) : T & (p 1 p 2) [C-Cast] [C-Let] Compilation of Types E T T E, x : B s t : {y :Bool u} & pure E {x:b s} {x:b t} S = x:[l i : f i p i (y :S i S i) i 1..n ].s U k = x:[l i : f i p i (y :T i T i ) i 1..k ] T = x:[l i : f i p i (y :T i T i ) i 1..n ].t E, x : U j 1 S j T j j 1..n E, x : U j 1, y : T j S j T j j 1..n E, x : U n s t : {y :Bool u} & pure E S T Compilation and Checking [C-Base] [C-ObjTy] E s t : T & p E s t : S & q E alg S <: T q p E s t T & p E s t : S & q E? alg S <: T q p E s ( T t) T & p [CC-Ok] [CC-Chk]
9 if s is well-typed, then all dynamic casts inserted into t will succeed. If s is not well-typed, then execution of t may potentially halt due to the failure of a compiler-inserted cast. We extend compilation to types as well, since they contain terms. The full set of compilation rules is shown in Figure 6. Many of these rules are straightforward. Variable references and constants never need additional casts, as evidenced by rules [C-Var] and [C-Const]. To compile an object (x.[l i(y) = s i i 1..n ] as S), the rule [C-Obj] first compiles the object type S into type T = x:[l i : f i p i (y :T i T i ) i 1..n ] and then compiles each method body s i into t i, which must have type y :T i T i. We use the compilation and checking judgment E s t T & p to both compile s into t and to ensure that t has type T (and purity p). The rules defining this judgment exhibit the key ideas behind hybrid type checking for objects. After compiling the term s into t (with type S), the subtyping algorithm E a alg S <: T is used to check if S is a subtype of T. - If the subtyping algorithm succeeds (i.e., E alg S <: T ), then no casts are needed: see [CC-Ok]. - If the subtyping algorithm disproves this subtyping requirement (i.e., E alg S <: T ), the program fails to compile, since no compilation rule is applicable. - If the subtyping algorithm cannot either prove or refute this subtyping requirement (i.e., E? alg S <: T ), then a dynamic cast from S to T is inserted around t via the rule [CC-Chk]. Ideally, the subtyping algorithm will be sufficiently complete to handle most cases definitively and casts will be inserted rarely. However, this crucial ability to add casts permits our compiler to support an unusually expressive object specification language. The compiler compiles types wherever they are found in the source program (i.e., in [C-Cast] and [C-Obj]), to ensure that all types mentioned in the compiled program are well-formed, and that all environments constructed during compilation are well-formed. 7. Correctness In this section, we establish important correctness properties of the Hoop type system and the hybrid compilation algorithm. 7.1 Correctness of the Type System We first extend the type system to run-time states, which contain an object store as well as object addresses and object views. In particular, we extend each typing judgment to include an object store σ, resulting in the extended judgment forms: σ; E t : T & p σ; E T σ; E S <: T σ; E M = N σ; E M <: N σ; E s t σ; E = θ Most of the extended type rules are identical to the original rules, except that they pass the additional store argument σ to their antecedents. The only exception is the following rule [Imp], which uses the store σ when evaluating implication predicates: θ. (σ; E = θ (σ, θ(t)) (σ, false)) (σ, θ(s)) (σ, false) σ; E s t [Imp] We introduce two new rules for checking object addresses and object views: σ(a) = x.[...] as T σ; E a : T & pure σ(a) = x.[l i(y) = t i i 1..n ] as S S = x:[l i : f i q i M i i 1..n ].s T = x:[l i : f i p i N i i 1..m ].t T = x:[l i : f i p i N i i 1..m ] m n q i p i i 1..m (σ, t[x := (a view T )]) (σ, true) σ; E a view T : T & pure Finally, we add rules for typing stores and states: dom(σ) = {a 1,..., a n} σ(a i) = x.[...] as S i i 1..n σ; σ(a i) : S i & pure σ σ σ; t : T & p (σ, t) : T [T-Obj-Ref] [T-Obj-View] [T-Store] [T-State] We assume that the type of each primitive operation is consistent with its operational behavior. Assumption 1 (Types of Primitives). If and [c](l, v, σ) = v then (σ, v ) : T. (σ, c.l(v)) : T The extended type system then satisfies the preservation or subject reduction property [41]. The type system also satisfies the progress property (i.e., the evaluation of welltyped programs does not halt prematurely), with the caveat that type casts may fail. A state (σ, E[ T v]) has a failed cast if it cannot be reduced via the rules [E-Cast-Base], [E-Cast-Obj], or [E-Cast-View]. Both theorems follow by induction over typing derivations. Theorem 2 (Preservation). If (σ, t) then (σ, t) : T. (σ, s) : T and (σ, s) Theorem 3 (Progress). All closed well-typed normal forms are values or contain a failed cast. 7.2 Correctness of Hybrid Type System We now describe the correctness properties of our hybrid type system. We assume that the implication algorithm is a sound approximation of the implication judgment: Assumption 4 (Soundness of E a alg s t). Suppose E. 1. If E alg s t then E s t. 2. If E alg s t then E s t. Given this assumption, our subtyping algorithm is sound: Lemma 5 (Soundness of E a alg S <: T ). Suppose E. 1. If E alg S <: T then E S <: T.
10 2. If E alg S <: T then E S <: T. Proof: By induction over algorithmic subtyping derivations. Also, the compilation algorithm inserts sufficient dynamic type casts to compensate for the inherent imprecisions of the subtyping algorithm, which ensures that compiled programs are always well-typed. Theorem 6 (Compiled Programs Are Well-typed). Suppose E. 1. If E s t : T & p then E t : T & p. 2. If E s t T & p and E T then E t : T & p. 3. If E S T then E T. Proof: By induction over compilation derivations. An immediate consequence of this lemma, when combined with Theorem 3 (Progress), is that compiled programs only halt prematurely due to failed casts. Such casts may be explicit in the original program or implicitly inserted by the compiler. Thus, for some subtle specification violations, hybrid type checking may only catch these errors via cast failures at run time. However, we argue that this precise hybrid approach may be superior to using a coarser type language that could not express subtle specifications at all. 8. Related Work Much prior work has focused on dynamic checking of expressive specifications, or contracts [29, 11, 24, 16, 20, 26, 34, 21]. An entire design philosophy, Contract Oriented Design, has been based on dynamically-checked specifications. Hybrid type checking extends these prior purely-dynamic approaches by verifying (or detecting violations of) expressive specifications statically, wherever possible. The programming language Eiffel [29] supports a notion of hybrid specifications by providing both statically-checked types as well as dynamically-checked contracts. Having separate (static and dynamic) specification languages is awkward, since it requires the programmer to factor each specification into its static and dynamic components. Furthermore, the specification may need to be manually refactored to exploit improvements in static checking technology. Our work shares similar motivations with, and is partly inspired by, recent work on advanced type systems, including work on refinement types [15, 28, 8] and practical dependent types [43, 42]. However, the requirement for full static decidability limits the expressiveness of these prior systems. Hybrid type checking side-steps these decidability difficulties by being willing to check correctness properties dynamically when necessary. The static checking tool ESC/Java [14] supports expressive JML specifications [24] and leverages powerful automatic theorem proving techniques. However, ESC/Java s underlying theorem prover, Simplify [9], does not distinguish between failing to prove a theorem and finding a counterexample that actually refutes the theorem. Consequently, ESC/Java may produce error messages that are caused by limitations in its theorem prover. In contrast, hybrid type checking only produces error messages for programs it can prove are ill-typed. Abadi and Leino [3] developed and proved the soundness of a Hoare-style logic for reasoning about pre- and post-conditions in an imperative object language. As with ESC/Java, this logic reduces program correctness to theorem proving, which is undecidable. Others have explored various semantic models [36] and extensions [19] to the Abadi-Leino system. Extending our work to support an imperative object language would require studying a number of additional verification issues, such as frame conditions [6] and aliasing/ownership [7, 31], that arise in an imperative setting. There have been a number of projects focused on refinement of specifications and subtyping. These include the work of Liskov and Wing [25], Leavens [23], Lano and Haughton [22], and others. Our notion of subtyping is simpler than many of these studies, and does not, for example, include data abstraction. One interesting avenue for future work is to explore these richer notions of subtyping and abstraction in the context of hybrid type checking. The limitations of purely-static and purely-dynamic approaches have also motivated other work on hybrid analyses. For example, CCured [30] is a hybrid analysis for preventing array bounds violations. Unlike our proposed approach, it does not detect errors statically - instead, the static analysis is used to optimize the run-time analysis. Specialized hybrid analyses have been proposed for other problems as well, such as race condition checking [39, 32, 4]. Recently, Ou et al presented a system leveraging dependent types and run-time checks [33], although their system does not include objects. In contrast to Hoop, their type system is decidable and leverages dynamic checks to reduce the need for precise type annotations in explicitly labeled regions of programs. The interaction between static typing and dynamic checks has been previously studied in context of flexible type systems with types such as the type Dynamic, which can be converted to other types [2]. Quasi-static typing [38] automatically inserts the necessary coercions, in a manner similar to soft typing [27, 40, 5, 13]. This work is intended to support looser type specifications. In contrast, our work uses similar, automatically-inserted casts to support more precise type specifications. An interesting avenue for further exploration is the combination of both approaches to support a very large range of specifications, from Dynamic (no static type information) at one extreme to very precise hybrid-checked specifications at the other. 9. Conclusions and Future Work This paper presents a hybrid type system that permits programmers to specify object interfaces precisely, using object invariants and type refinements, and to delegate to the hybrid compiler decisions regarding which parts of these specifications can be checked statically, and which must be checked dynamically. A number of issues remain for future work, including experimental validation. The desire for static decidability has often constrained traditional object type systems. We believe that hybrid type checking may facilitate the design of programming languages around expressive type systems that balance safety with flexibility, and whose undecidability need not limit their practicality. Acknowledgments This work was supported by the National Science Foundation under Grants CCR and CCR We thank Martín Abadi for helpful comments on this work. References [1] M. Abadi and L. Cardelli. A Theory of Objects. Springer- Verlag, 1996.
11 [2] M. Abadi, L. Cardelli, B. Pierce, and G. Plotkin. Dynamic typing in a statically-typed language. In Proceedings of the ACM Symposium on Principles of Programming Languages, pages , [3] M. Abadi and K. R. M. Leino. A logic of object-oriented programs. In Verification: Theory and Practice, pages 11 41, [4] R. Agarwal and S. D. Stoller. Type inference for parameterized race-free Java. In Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation, pages , [5] A. Aiken, E. L. Wimmers, and T. K. Lakshman. Soft typing with conditional types. In Proceedings of the ACM Symposium on Principles of Programming Languages, pages , [6] A. Borgida, J. Mylopoulos, and R. Reiter. On the frame problem in procedure specifications. IEEE Trans. Software Eng., 21(10): , [7] J. Boyland, J. Noble, and W. Retert. Capabilities for sharing: A generalisation of uniqueness and read-only. In Proceedings of the European Conference on Object Oriented Programming, pages 2 27, [8] R. Davies and F. Pfenning. Intersection types and computational effects. In Proceedings of the ACM International Conference on Functional Programming, pages , [9] D. Detlefs, G. Nelson, and J. B. Saxe. Simplify: a theorem prover for program checking. J. ACM, 52(3): , [10] ECMA. Standard ECMA-334: C# Language Specification (3rd edition), Available on the web as files/ecma-st/ecma-334.pdf. [11] R. B. Findler and M. Felleisen. Contracts for higher-order functions. In Proceedings of the International Conference on Functional Programming, pages 48 59, [12] C. Flanagan. Hybrid type checking. In Proceedings of the ACM Symposium on Principles of Programming Languages, [13] C. Flanagan, M. Flatt, S. Krishnamurthi, S. Weirich, and M. Felleisen. Finding bugs in the web of program invariants. In Proceedings of the ACM Conference on Programming Language Design and Implementation, pages 23 32, [14] C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for Java. In Proceedings of the ACM Conference on Programming Language Design and Implementation, pages , [15] T. Freeman and F. Pfenning. Refinement types for ML. In Proceedings of the ACM Conference on Programming Language Design and Implementation, pages , [16] B. Gomes, D. Stoutamire, B. Vaysman, and H. Klawitter. A language manual for Sather 1.1, [17] J. Gosling, B. Joy, G. Steele, and G. Bracha. The Java Language Specification (3rd Edition). Addison-Wesley, [18] J. Gronski, K. Knowles, A. Tomb, S. N. Freund, and C. Flanagan. Sage: Practical hybrid checking for expressive types and specifications, extended report. to appear, [19] M. Hofmann and F. Tang. Implementing a program logic of objects in a higher-order logic theorem prover. In Proceedings of the Conference on Theorem Proving in Higher Order Logics, pages , [20] R. C. Holt and J. R. Cordy. The Turing programming language. Communications of the ACM, 31: , [21] M. Kölling and J. Rosenberg. Blue: Language specification, version 0.94, [22] K. Lano and H. P. Haughton. Reasoning and refinement in object-oriented specification languages. In Proceedings of the European Conference on Object Oriented Programming, pages 78 97, [23] G. T. Leavens. Reasoning about Object-Oriented Programs that Use Subtypes. PhD thesis, Massachusetts Institute of Technology, [24] G. T. Leavens and Y. Cheon. Design by contract with JML, avaiable at [25] B. Liskov and J. M. Wing. A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems, 16(6): , [26] D. Luckham. Programming with specifications. Texts and Monographs in Computer Science, [27] M. Fagan. Soft Typing. PhD thesis, Rice University, [28] Y. Mandelbaum, D. Walker, and R. Harper. An effective theory of type refinements. In Proceedings of the International Conference on Functional Programming, pages , [29] B. Meyer. Object-oriented Software Construction. Prentice Hall, [30] G. C. Necula, S. McPeak, and W. Weimer. CCured: typesafe retrofitting of legacy code. In Proceedings of the ACM Symposium on Principles of Programming Languages, pages , [31] J. Noble, J. Vitek, and J. Potter. Flexible alias protection. In Proceedings of the European Conference on Object Oriented Programming, pages , [32] R. O Callahan and J.-D. Choi. Hybrid dynamic data race detection. In ACM Symposium on Principles and Practice of Parallel Programming, pages , [33] X. Ou, G. Tan, Y. Mandelbaum, and D. Walker. Dynamic typing with dependent types. In IFIP International Conference on Theoretical Computer Science, pages , [34] D. L. Parnas. A technique for software module specification with examples. Communications of the ACM, 15(5): , [35] D. Rémy and J. Vouillon. Objective ML: An effective objectoriented extension to ML. Theory And Practice of Object Systems, 4(1):27 50, [36] B. Reus and J. Schwinghammer. Denotational semantics for Abadi and Leino s logic of objects. In Proceedings of the European Symposium on Programming, pages , [37] D. S. Rosenblum. A practical approach to programming with assertions. IEEE Transactions on Software Engineering, 21(1):19 31, [38] S. Thatte. Quasi-static typing. In Proceedings of the ACM Symposium on Principles of Programming Languages, pages , [39] C. von Praun and T. Gross. Object race detection. In Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages and Applications, pages 70 82, [40] A. Wright and R. Cartwright. A practical soft type system for scheme. In Proceedings of the ACM Conference on Lisp and Functional Programming, pages , [41] A. Wright and M. Felleisen. A syntactic approach to type soundness. Info. Comput., 115(1):38 94, [42] H. Xi. Imperative programming with dependent types. In Proceedings of the IEEE Symposium on Logic in Computer Science, pages , [43] H. Xi and F. Pfenning. Dependent types in practical programming. In Proceedings of the ACM Symposium on Principles of Programming Languages, pages , 1999.
Hybrid Type Checking
Hybrid Type Checking Cormac Flanagan Department of Computer Science University of California, Santa Cruz email@example.com Abstract Traditional static type systems are very effective for verifying basicMore information
Well-typed programs can t be blamed
Well-typed programs can t be blamed Philip Wadler University of Edinburgh Robert Bruce Findler University of Chicago Abstract We introduce the blame calculus, which adds the notion of blame from FindlerMore information
Extended Static Checking for Java
Lukas TU München - Seminar Verification 14. Juli 2011 Outline 1 Motivation 2 ESC/Java example 3 ESC/JAVA architecture VC generator Simplify 4 JML + ESC/Java annotation language JML What ESC/Java checksMore information
Sage: Unified Hybrid Checking for First-Class Types, General Refinement Types, and Dynamic (Extended Report)
Sage: Unified Hybrid Checking for First-Class Types, General Refinement Types, and Dynamic (Extended Report) Kenneth Knowles Aaron Tomb Jessica Gronski Stephen N. Freund Cormac Flanagan University of California,More information
Types, Polymorphism, and Type Reconstruction
Types, Polymorphism, and Type Reconstruction Sources This material is based on the following sources: Pierce, B.C., Types and Programming Languages. MIT Press, 2002. Kanellakis, P.C., Mairson, H.G. andMore information
Specification and Analysis of Contracts Lecture 1 Introduction
Specification and Analysis of Contracts Lecture 1 Introduction Gerardo Schneider firstname.lastname@example.com http://folk.uio.no/gerardo/ Department of Informatics, University of Oslo SEFM School, Oct. 27 - Nov.More information
Behavioral Contracts and Behavioral Subtyping
Behavioral ontracts and Behavioral Subtyping Robert Bruce Findler Rice University 6100 South Main; MS 132 Houston, TX 77006; USA Mario Latendresse Rice University Matthias Felleisen Rice University NortheasternMore information
Checking Access to Protected Members in the Java Virtual Machine
Checking Access to Protected Members in the Java Virtual Machine Alessandro Coglio Kestrel Institute 3260 Hillview Avenue, Palo Alto, CA 94304, USA Ph. +1-650-493-6871 Fax +1-650-424-1807 http://www.kestrel.edu/More information
The gradual typing approach to mixing static and dynamic typing
1/38 The gradual typing approach to mixing static and dynamic typing Jeremy G. Siek University of Colorado =) Indiana University TFP 2013 at Provo, Utah, May 2013 The Goals of Gradual Typing I Enjoy theMore information
On the Relation between Design Contracts and Errors: A Software Development Strategy
On the Relation between Design Contracts and Errors: A Software Development Strategy Eivind J. Nordby, Martin Blom, Anna Brunstrom Computer Science, Karlstad University SE-651 88 Karlstad, Sweden {Eivind.Nordby,More information
A Framework for the Semantics of Behavioral Contracts
A Framework for the Semantics of Behavioral Contracts Ashley McNeile Metamaxim Ltd, 48 Brunswick Gardens, London W8 4AN, UK firstname.lastname@example.com Abstract. Contracts have proved a powerful conceptMore information
Rigorous Software Development CSCI-GA 3033-009
Rigorous Software Development CSCI-GA 3033-009 Instructor: Thomas Wies Spring 2013 Lecture 5 Disclaimer. These notes are derived from notes originally developed by Joseph Kiniry, Gary Leavens, Erik Poll,More information
InvGen: An Efficient Invariant Generator
InvGen: An Efficient Invariant Generator Ashutosh Gupta and Andrey Rybalchenko Max Planck Institute for Software Systems (MPI-SWS) Abstract. In this paper we present InvGen, an automatic linear arithmeticMore information
Rigorous Software Development CSCI-GA 3033-009
Rigorous Software Development CSCI-GA 3033-009 Instructor: Thomas Wies Spring 2013 Lecture 11 Semantics of Programming Languages Denotational Semantics Meaning of a program is defined as the mathematicalMore information
Automated Theorem Proving - summary of lecture 1
Automated Theorem Proving - summary of lecture 1 1 Introduction Automated Theorem Proving (ATP) deals with the development of computer programs that show that some statement is a logical consequence ofMore information
Programming Languages Featherweight Java David Walker
Programming Languages Featherweight Java David Walker Overview Featherweight Java (FJ), a minimal Javalike language. Models inheritance and subtyping. Immutable objects: no mutation of fields. TrivializedMore information
Verifying Semantic of System Composition for an Aspect-Oriented Approach
2012 International Conference on System Engineering and Modeling (ICSEM 2012) IPCSIT vol. 34 (2012) (2012) IACSIT Press, Singapore Verifying Semantic of System Composition for an Aspect-Oriented ApproachMore information
Design by Contract beyond class modelling
Design by Contract beyond class modelling Introduction Design by Contract (DbC) or Programming by Contract is an approach to designing software. It says that designers should define precise and verifiableMore information
[Refer Slide Time: 05:10]
Principles of Programming Languages Prof: S. Arun Kumar Department of Computer Science and Engineering Indian Institute of Technology Delhi Lecture no 7 Lecture Title: Syntactic Classes Welcome to lectureMore information
Introducing Formal Methods. Software Engineering and Formal Methods
Introducing Formal Methods Formal Methods for Software Specification and Analysis: An Overview 1 Software Engineering and Formal Methods Every Software engineering methodology is based on a recommendedMore information
Chair of Software Engineering. Software Verification. Assertion Inference. Carlo A. Furia
Chair of Software Engineering Software Verification Assertion Inference Carlo A. Furia Proving Programs Automatically The Program Verification problem: Given: a program P and a specification S = [Pre,More information
Functional Programming. Functional Programming Languages. Chapter 14. Introduction
Functional Programming Languages Chapter 14 Introduction Functional programming paradigm History Features and concepts Examples: Lisp ML 1 2 Functional Programming Functional Programming Languages TheMore information
International Journal of Computer ScienceandCommunication Vol. 2, No. 1, January-June2011, pp. 153-157 PROPERTECHNIQUEOFSOFTWARE INSPECTIONUSING GUARDED COMMANDLANGUAGE Neeraj Kumar Singhania University,More information
Indexed Types in Object-Oriented Programming
Indexed Types in Object-Oriented Programming Joana Campos and Vasco T. Vasconcelos University of Lisbon, Faculty of Sciences, LaSIGE Abstract. Dependent type systems allow semantic properties to be expressedMore information
Object-Oriented Software Specification in Programming Language Design and Implementation
Object-Oriented Software Specification in Programming Language Design and Implementation Barrett R. Bryant and Viswanathan Vaidyanathan Department of Computer and Information Sciences University of AlabamaMore information
Praspel: A Specification Language for Contract-Driven Testing in PHP
Praspel: A Specification Language for Contract-Driven Testing in PHP Ivan Enderlin Frédéric Dadeau Alain Giorgetti Abdallah Ben Othman October 27th, 2011 Meetings: LTP MTVV Ivan Enderlin, Frédéric Dadeau,More information
Journal of Functional Programming, volume 3 number 4, 1993. Dynamics in ML
Journal of Functional Programming, volume 3 number 4, 1993. Dynamics in ML Xavier Leroy École Normale Supérieure Michel Mauny INRIA Rocquencourt Abstract Objects with dynamic types allow the integrationMore information
JOURNAL OF OBJECT TECHNOLOGY Online at www.jot.fm. Published by ETH Zurich, Chair of Software Engineering JOT, 2002 Vol. 1, No. 3 Special issue: TOOLS USA 2002 proceedings Evaluation of Assertion SupportMore information
Termination Checking: Comparing Structural Recursion and Sized Types by Examples
Termination Checking: Comparing Structural Recursion and Sized Types by Examples David Thibodeau Decemer 3, 2011 Abstract Termination is an important property for programs and is necessary for formal proofsMore information
StaRVOOrS: A Tool for Combined Static and Runtime Verification of Java
StaRVOOrS: A Tool for Combined Static and Runtime Verification of Java Jesús Mauricio Chimento 1, Wolfgang Ahrendt 1, Gordon J. Pace 2, and Gerardo Schneider 3 1 Chalmers University of Technology, Sweden.More information
Type Classes with Functional Dependencies
Appears in Proceedings of the 9th European Symposium on Programming, ESOP 2000, Berlin, Germany, March 2000, Springer-Verlag LNCS 1782. Type Classes with Functional Dependencies Mark P. Jones DepartmentMore information
Dsc+Mock: A Test Case + Mock Class Generator in Support of Coding Against Interfaces
Dsc+Mock: A Test Case + Mock Class Generator in Support of Coding Against Interfaces Mainul Islam, Christoph Csallner Computer Science and Engineering Department University of Texas at Arlington Arlington,More information
Blame for All. Jeremy G. Siek. Amal Ahmed. Robert Bruce Findler. Philip Wadler. Abstract. 1. Introduction
Blame for All Amal Ahmed Indiana University firstname.lastname@example.com Robert Bruce Findler Northwestern University firstname.lastname@example.com Jeremy G. Siek University of Colorado at Boulder email@example.com information
Rigorous Software Engineering Hoare Logic and Design by Contracts
Rigorous Software Engineering Hoare Logic and Design by Contracts Simão Melo de Sousa RELEASE (UBI), LIACC (Porto) Computer Science Department University of Beira Interior, Portugal 2010-2011 S. Melo deMore information
The Trip Scheduling Problem
The Trip Scheduling Problem Claudia Archetti Department of Quantitative Methods, University of Brescia Contrada Santa Chiara 50, 25122 Brescia, Italy Martin Savelsbergh School of Industrial and SystemsMore information
Trust but Verify: Authorization for Web Services. The University of Vermont
Trust but Verify: Authorization for Web Services Christian Skalka X. Sean Wang The University of Vermont Trust but Verify (TbV) Reliable, practical authorization for web service invocation. Securing complexMore information
Comp 411 Principles of Programming Languages Lecture 34 Semantics of OO Languages. Corky Cartwright Swarat Chaudhuri November 30, 20111
Comp 411 Principles of Programming Languages Lecture 34 Semantics of OO Languages Corky Cartwright Swarat Chaudhuri November 30, 20111 Overview I In OO languages, data values (except for designated non-ooMore information
Adapting C++ Exception Handling to an Extended COM Exception Model
Adapting C++ Exception Handling to an Extended COM Exception Model Bjørn Egil Hansen DNV AS, DT 990 Risk Management Software Palace House, 3 Cathedral Street, London SE1 9DE, UK firstname.lastname@example.com information
Applying Search in an Automatic Contract-Based Testing Tool
Applying Search in an Automatic Contract-Based Testing Tool Alexey Kolesnichenko, Christopher M. Poskitt, and Bertrand Meyer ETH Zürich, Switzerland Abstract. Automated random testing has been shown toMore information
Chapter 7: Functional Programming Languages
Chapter 7: Functional Programming Languages Aarne Ranta Slides for the book Implementing Programming Languages. An Introduction to Compilers and Interpreters, College Publications, 2012. Fun: a languageMore information
Software Testing & Analysis (F22ST3): Static Analysis Techniques 2. Andrew Ireland
Software Testing & Analysis (F22ST3) Static Analysis Techniques Andrew Ireland School of Mathematical and Computer Science Heriot-Watt University Edinburgh Software Testing & Analysis (F22ST3): StaticMore information
AURA: A language with authorization and audit
AURA: A language with authorization and audit Steve Zdancewic University of Pennsylvania WG 2.8 2008 Security-oriented Languages Limin Jia, Karl Mazurak, Jeff Vaughan, Jianzhou Zhao Joey Schorr and LukeMore information
Constructing Contracts: Making Discrete Mathematics Relevant to Beginning Programmers
Constructing Contracts: Making Discrete Mathematics Relevant to Beginning Programmers TIMOTHY S. GEGG-HARRISON Winona State University Although computer scientists understand the importance of discreteMore information
Chapter 5 Names, Bindings, Type Checking, and Scopes
Chapter 5 Names, Bindings, Type Checking, and Scopes Chapter 5 Topics Introduction Names Variables The Concept of Binding Type Checking Strong Typing Scope Scope and Lifetime Referencing Environments NamedMore information
The Clean programming language. Group 25, Jingui Li, Daren Tuzi
The Clean programming language Group 25, Jingui Li, Daren Tuzi The Clean programming language Overview The Clean programming language first appeared in 1987 and is still being further developed. It wasMore information
Type Systems. Luca Cardelli. Microsoft Research
Type Systems Luca Cardelli Microsoft Research 1 Introduction The fundamental purpose of a type system is to prevent the occurrence of execution errors during the running of a program. This informal statementMore information
Journal of Computer Security draft printout, (17 Sep 2009), 1 20 IOS Press 1 A SOUND TYPE SYSTEM FOR SECURE FLOW ANALYSIS Dennis Volpano Computer Science Department Naval Postgraduate School Monterey,More information
Simulation-Based Security with Inexhaustible Interactive Turing Machines
Simulation-Based Security with Inexhaustible Interactive Turing Machines Ralf Küsters Institut für Informatik Christian-Albrechts-Universität zu Kiel 24098 Kiel, Germany email@example.com information
Data Abstraction and Hierarchy
Data Abstraction and Hierarchy * This research was supported by the NEC Professorship of Software Science and Engineering. Barbara Liskov Affiliation: MIT Laboratory for Computer Science Cambridge, MA,More information
Functional Programming
FP 2005 1.1 3 Functional Programming WOLFRAM KAHL email@example.com Department of Computing and Software McMaster University FP 2005 1.2 4 What Kinds of Programming Languages are There? Imperative tellingMore information
Determination of the normalization level of database schemas through equivalence classes of attributes
Computer Science Journal of Moldova, vol.17, no.2(50), 2009 Determination of the normalization level of database schemas through equivalence classes of attributes Cotelea Vitalie Abstract In this paper,More information
Theory of Computation Lecture Notes
Theory of Computation Lecture Notes Abhijat Vichare August 2005 Contents 1 Introduction 2 What is Computation? 3 The λ Calculus 3.1 Conversions: 3.2 The calculus in use 3.3 Few Important Theorems 3.4 WorkedMore information
Formal Verification Coverage: Computing the Coverage Gap between Temporal Specifications
Formal Verification Coverage: Computing the Coverage Gap between Temporal Specifications Sayantan Das Prasenjit Basu Ansuman Banerjee Pallab Dasgupta P.P. Chakrabarti Department of Computer Science & EngineeringMore information
2. Methods of Proof Types of Proofs. Suppose we wish to prove an implication p q. Here are some strategies we have available to try.
2. METHODS OF PROOF 69 2. Methods of Proof 2.1. Types of Proofs. Suppose we wish to prove an implication p q. Here are some strategies we have available to try. Trivial Proof: If we know q is true thenMore information
Pluggable Type Systems. Gilad Bracha
Pluggable Type Systems Gilad Bracha The Paradox of Type Systems Type systems help reliability and security by mechanically proving program properties Type systems hurt reliability and security by makingMore information
ML for the Working Programmer
ML for the Working Programmer 2nd edition Lawrence C. Paulson University of Cambridge CAMBRIDGE UNIVERSITY PRESS CONTENTS Preface to the Second Edition Preface xiii xv 1 Standard ML 1 Functional ProgrammingMore information
Two Flavors in Automated Software Repair: Rigid Repair and Plastic Repair
Two Flavors in Automated Software Repair: Rigid Repair and Plastic Repair Martin Monperrus, Benoit Baudry Dagstuhl Preprint, Seminar #13061, 2013. Link to the latest version Abstract In this paper, weMore information
Computer-Assisted Theorem Proving for Assuring the Correct Operation of Software
1 Computer-Assisted Theorem Proving for Assuring the Correct Operation of Software Amy Felty University of Ottawa Introduction to CSI5110 2 The General Problem From Evan I. Schwartz, Trust Me, I m YourMore information
Testing LTL Formula Translation into Büchi Automata
Testing LTL Formula Translation into Büchi Automata Heikki Tauriainen and Keijo Heljanko Helsinki University of Technology, Laboratory for Theoretical Computer Science, P. O. Box 5400, FIN-02015 HUT, FinlandMore information
Appendix... B. The Object Constraint
UML 2.0 in a Nutshell Appendix B. The Object Constraint Pub Date: June 2005 Language The Object Constraint Language 2.0 (OCL) is an addition to the UML 2.0 specification that provides you with a way toMore information
4 Domain Relational Calculus
4 Domain Relational Calculus We now present two relational calculi that we will compare to RA. First, what is the difference between an algebra and a calculus? The usual story is that the algebra RA isMore information
OPERATIONAL TYPE THEORY by Adam Petcher Prepared under the direction of Professor Aaron Stump A thesis presented to the School of Engineering of
WASHINGTON NIVERSITY SCHOOL OF ENGINEERING AND APPLIED SCIENCE DEPARTMENT OF COMPTER SCIENCE AND ENGINEERING DECIDING JOINABILITY MODLO GROND EQATIONS IN OPERATIONAL TYPE THEORY by Adam Petcher PreparedMore information
Computing and Informatics, Vol. 20, 2001,????, V 2006-Nov-6 UPDATES OF LOGIC PROGRAMS Ján Šefránek Department of Applied Informatics, Faculty of Mathematics, Physics and Informatics, Comenius University,More information
THE IMPACT OF INHERITANCE ON SECURITY IN OBJECT-ORIENTED DATABASE SYSTEMS David L. Spooner Computer Science Department Rensselaer Polytechnic Institute Troy, New York 12180 The object-oriented programmingMore information
A Reverse Inheritance Relationship for Improving Reusability and Evolution: The Point of View of Feature Factorization
Reverse Inheritance Relationship for Improving Reusability and Evolution: The Point of View of Feature Factorization Ciprian-Bogdan Chirila *, Pierre Crescenzo **, and Philippe Lahire ** * University PolitehnicaMore information
Computer Programming I
Computer Programming I COP 2210 Syllabus Spring Semester 2012 Instructor: Greg Shaw Office: ECS 313 (Engineering and Computer Science Bldg) Office Hours: Tuesday: 2:50 4:50, 7:45 8:30 Thursday: 2:50 4:50,More information
Department of Computing Science and Mathematics University of Stirling
Department of Computing Science and Mathematics University of Stirling Push-Button Tools for Application Developers, Full Formal Verification for Component Vendors Thomas Wilson, Savi Maharaj, Robert G.More information
Chapter 7 Application Protocol Reference Architecture
Application Protocol Reference Architecture Chapter 7 Application Protocol Reference Architecture This chapter proposes an alternative reference architecture for application protocols. The proposed referenceMore information
Programming Languages
Programming Languages Qing Yi Course web site: www.cs.utsa.edu/~qingyi/cs3723 cs3723 1 A little about myself Qing Yi Ph.D. Rice University, USA. Assistant Professor, Department of Computer Science Office:More information
OUR WORK takes place in the process described in [2]
Reverse-engineering of UML 2.0 Sequence Diagrams from Execution Traces Romain Delamare, Benoit Baudry IRISA / INRIA Rennes Campus Universitaire de Beaulieu Avenue du Général Leclerc 35042 Rennes CedexMore information
Chapter 15 Functional Programming Languages
Chapter 15 Functional Programming Languages Introduction - The design of the imperative languages is based directly on the von Neumann architecture Efficiency (at least at first) is the primary concern,More information
A Scala DSL for Rete-based Runtime Verification
A Scala DSL for Rete-based Runtime Verification Klaus Havelund Jet Propulsion Laboratory California Institute of Technology, California, USA Abstract. Runtime verification (RV) consists in part of checkingMore information
Coverability for Parallel Programs
2015 http://excel.fit.vutbr.cz Coverability for Parallel Programs Lenka Turoňová* Abstract We improve existing method for the automatic verification of systems with parallel running processes. The techniqueMore information
A Type System for Data-Flow Integrity on Windows Vista
A Type System for Data-Flow Integrity on Windows Vista Avik Chaudhuri University of California at Santa Cruz email@example.com Prasad Naldurg Sriram Rajamani Microsoft Research India {prasadn,firstname.lastname@example.com information
Towards a Framework for Generating Tests to Satisfy Complex Code Coverage in Java Pathfinder
Towards a Framework for Generating Tests to Satisfy Complex Code Coverage in Java Pathfinder Matt Department of Computer Science and Engineering University of Minnesota firstname.lastname@example.com Abstract We presentMore information
From Program Verification to Certified Binaries
From Program Verification to Certified Binaries The Quest for the Holy Grail of Software Engineering Angelos Manousaridis, Michalis A. Papakyriakou, and Nikolaos S. Papaspyrou National Technical UniversityMore information
Parametric Domain-theoretic models of Linear Abadi & Plotkin Logic
Parametric Domain-theoretic models of Linear Abadi & Plotkin Logic Lars Birkedal Rasmus Ejlers Møgelberg Rasmus Lerchedahl Petersen IT University Technical Report Series TR-00-7 ISSN 600 600 February 00More information
SOLUTIONS TO ASSIGNMENT 1 MATH 576 SOLUTIONS BY OLIVIER MARTIN 13 #5. Let T be the topology generated by A on X. We want to show T = J B J where B is the set of all topologies J on X with A J. This amountsMore information
Checks and Balances - Constraint Solving without Surprises in Object-Constraint Programming Languages
Checks and Balances - Constraint Solving without Surprises in Object-Constraint Programming Languages Tim Felgentreff, Todd Millstein, Alan Borning and Robert Hirschfeld Viewpoints Research Institute,More information
Compiling Object Oriented Languages. What is an Object-Oriented Programming Language? Implementation: Dynamic Binding
Compiling Object Oriented Languages What is an Object-Oriented Programming Language? Last time Dynamic compilation Today Introduction to compiling object oriented languages What are the issues? ObjectsMore information
Automatic Verification by Abstract Interpretation
Automatic Verification by Abstract Interpretation (Invited tutorial) Patrick Cousot École normale supérieure, Département d informatique, 45 rue d Ulm, 75230 Paris cedex 05, France email@example.com information
Semantic Analysis: Types and Type Checking
Semantic Analysis Semantic Analysis: Types and Type Checking CS 471 October 10, 2007 Source code Lexical Analysis tokens Syntactic Analysis AST Semantic Analysis AST Intermediate Code Gen lexical errorsMore information
Chapter II. Controlling Cars on a Bridge
Chapter II. Controlling Cars on a Bridge 1 Introduction The intent of this chapter is to introduce a complete example of a small system development. During this development, you will be made aware of theMore information
Transparent Monitoring of a Process Self in a Virtual Environment
Transparent Monitoring of a Process Self in a Virtual Environment PhD Lunchtime Seminar Università di Pisa 24 Giugno 2008 Outline Background Process Self Attacks Against the Self Dynamic and Static AnalysisMore information
Static Program Transformations for Efficient Software Model Checking
Static Program Transformations for Efficient Software Model Checking Shobha Vasudevan Jacob Abraham The University of Texas at Austin Dependable Systems Large and complex systems Software faults are majorMore information
2.3 Scheduling jobs on identical parallel machines
2.3 Scheduling jobs on identical parallel machines There are jobs to be processed, and there are identical machines (running in parallel) to which each job may be assigned Each job = 1,,, must be processedMore information
On Understanding Types, Data Abstraction, and Polymorphism
On Understanding Types, Data Abstraction, and Polymorphism LUCA CARDELLI AT&T Bell Laboratories, Murray Hill, N. J. 07974 PETER WEGNER Department of Computer Science, Brown University, Providence, R. I.More information
The countdown problem
JFP 12 (6): 609 616, November 2002. c 2002 Cambridge University Press DOI: 10.1017/S0956796801004300 Printed in the United Kingdom 609 F U N C T I O N A L P E A R L The countdown problem GRAHAM HUTTONMore information
CHAPTER 7 GENERAL PROOF SYSTEMS 1 Introduction Proof systems are built to prove statements. They can be thought as an inference machine with special statements, called provable statements, or sometimesMore information
On Understanding Types, Data Abstraction, and Polymorphism
1 Computing Surveys, Vol 17 n. 4, pp 471-522, December 1985 On Understanding Types, Data Abstraction, and Polymorphism Luca Cardelli AT&T Bell Laboratories, Murray Hill, NJ 07974 (current address: DECMore information
CCured: Type-Safe Retrofitting of Legacy Software
pdfauthor CCured: Type-Safe Retrofitting of Legacy Software GEORGE C. NECULA, JEREMY CONDIT, MATTHEW HARREN, SCOTT McPEAK, and WESTLEY WEIMER University of California, Berkeley This paper describes CCured,More information
Reasoning about Safety Critical Java
Reasoning about Safety Critical Java Chris Marriott 27 th January 2011 Motivation Safety critical systems are becoming part of everyday life Failure can potentially lead to serious consequences VerificationMore information
The Halting Problem is Undecidable
185 Corollary G = { M, w w L(M) } is not Turing-recognizable. Proof. = ERR, where ERR is the easy to decide language: ERR = { x { 0, 1 }* x does not have a prefix that is a valid code for a Turing machineMore information
Organization of Programming Languages CS320/520N. Lecture 05. Razvan C. Bunescu School of Electrical Engineering and Computer Science bunescu@ohio.
Organization of Programming Languages CS320/520N Razvan C. Bunescu School of Electrical Engineering and Computer Science email@example.com Names, Bindings, and Scopes A name is a symbolic identifier usedMore information
Language-Independent Model Transformation Verification K. Lano, S. Kolahdouz-Rahimi, T. Clark King s College London; University of Middlesex
Language-Independent Model Transformation Verification K. Lano, S. Kolahdouz-Rahimi, T. Clark King s College London; University of Middlesex 1 Language-independent MT verification One hinderance to MTMore information
Detecting Race Conditions in Large Programs
Detecting Race Conditions in Large Programs Cormac Flanagan Stephen N. Freund Compaq Systems Research Center 130 Lytton Ave. Palo Alto, CA 94301 {cormac.flanagan, email@example.com ABSTRACT TheMore information
3 Extending the Refinement Calculus
Building BSP Programs Using the Refinement Calculus D.B. Skillicorn? Department of Computing and Information Science Queen s University, Kingston, Canada firstname.lastname@example.com Abstract. We extend theMore information
A Parameterized Type System for Race-Free Java Programs
ACM Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), October 2001 A Parameterized Type System for Race-Free Java Programs Chandrasekhar Boyapati Martin Rinard LaboratoryMore information
Moving from CS 61A Scheme to CS 61B Java
Moving from CS 61A Scheme to CS 61B Java Introduction Java is an object-oriented language. This document describes some of the differences between object-oriented programming in Scheme (which we hope youMore information
Type Systems. Luca Cardelli. Digital Equipment Corporation Systems Research Center
Type Systems 1 Introduction Luca Cardelli Digital Equipment Corporation Systems Research Center The fundamental purpose of a type system is to prevent the occurrence of execution errors during the runningMore information


text:
15th-17th September 2017
Organised by the NSRA and Shakespeare County Raceway, another hot rod meet rolled up into a weekend of nostalgia style drag racing. Run what ya brung for pre-1973 cars. Hot rods, customs, Outlaw Anglias, dragsters, altereds, the Gasser Circus, and the flathead meltdown!
Shakespeare County Raceway
Long Marston Airfield
Long Marston
Stratford-upon-Avon CV37 8LL
Where else can you expect to see period Flathead roadsters and coupes, 200 mph blown methanol injected hot rods, ground thumping dragsters, big blocked Fiats and classic blown Willys Coupes? At the Original Hot Rod Drags of course!
Adding spice to the mix are the high riding gassers known as the Gasser Circus featuring high riding 'door cars' from the 40s, 50s and 60s. Along for the ride will be the Custom Car magazine supported Flathead Meltdown Challenge where side valve engines still reign supreme and last, but certainly no means least, the full on power from the awesome Outlaw Anglia class will be here to entertain in a class dedicated to Dagenham's finest 'sit up and beg' Anglias, Populars, Prefects and Fordsons.
Within the ranks of the nostalgia world expect to see out and out racers in the Wild Bunch class; a class which runs front engined 'slingshot' dragster and altereds where straight six Jaguars rub shoulders with Buick 'nailheads' as well as all kinds of Fords, Chryslers and of course Chevy V8's. The Outlaw Flat Four VW's will be looking for some more wheels up action with their classic VW gassers.
More on the Shakespeare County Raceway web site..
Some photos from a previous event. Click images to enlarge and browse..

subset: commoncrawl


text:
With league play just a few weeks away, there are a number of tradition-rich programs that are looking for fixes to the problems that have plagued them so far this season. For the teams whose play has been "under the weather," so to speak, they'll need more than a cup of chicken soup and extra rest to get back on track.
The good news is that during winter break (after final exams), the NCAA allows coaches unlimited time to work with their teams. It is not uncommon for coaches to have multiple practices a day in addition to team and individual film sessions.
This is a pivotal time for even the healthiest of programs, but for ones with flu-like symptoms, the next two weeks is the last window of opportunity to find the right formula for a full recovery.
Let's take a look at five programs -- including North Carolina and Texas, which play each other Wednesday night (9 ET, ESPN2) -- that have struggled to start the season, and the chances for each to turn things around.
Kentucky Wildcats
John Calipari's Wildcats are young even for his standards. No team in the nation lost more from last season's team and relies more on freshmen than Kentucky. Many forget that last season's championship prescription relied heavily upon three players who had experience and were invested in winning (Terrence Jones, Doron Lamb and Darius Miller). Those three players took to coaching and the weight room, and set the tone for a gifted freshman class.
This season's Wildcats team has suffered from numerous ailments, including below-average point guard play. But most of all, the young Cats are learning on the fly how to prepare and how to not take off plays.
The challenge for Calipari is that he needs to coach his team and push his team while keeping them confident. This is made more complicated by the fact that he doesn't have a player to coach his locker room and explain to his young Wildcats that there is a method to Cal's intensity and demanding coaching style.
I do feel that these Wildcats are starting to figure it out. Ryan Harrow is playing with more confidence, making better decisions and competing harder on the defensive end, which allows Archie Goodwin to play off the ball. Alex Poythress is more consistent and is poised to be a dominant player come SEC play, while Nerlens Noel is playing harder and is more alert and making better decisions on the defensive end.
My expectation for the Wildcats is that they will take a major step forward during Camp Cal and will once again be a factor come March.
Michigan State Spartans
Despite a tough early schedule and disappointing losses to Connecticut and at Miami, I feel Dr. Tom Izzo will find the right prescription to cure the Spartans' early-season headaches. Izzo is one of the best tournament coaches in recent college basketball history, and his ability to prioritize what is important, teach every day and adjust his system to his players always makes his teams a tough out come March.
The Spartans have a backcourt with the potential to be dynamic in Keith Appling and Gary Harris. As Harris adjusts to Izzo's system and the intensity of college basketball, he has the potential to be special by season's end. Appling is developing into a big-time playmaker in short-clock and late-game situations. The backcourt is deep with play-starter Travis Trice and skilled 6-foot-6 freshman Denzel Valentine. Branden Dawson, a natural small forward who can swing to the 4, is a tough matchup at both positions. He is an explosive athlete who rebounds and attacks the basket.
The challenge for Michigan State is how to get more consistency out of big men Adreian Payne and Derrick Nix. I expect Izzo will solve that issue, and that once again the Spartans will make a deep run in the NCAA tournament.
North Carolina Tar Heels
The Tar Heels are a team in transition, having lost four players to the first round of the NBA draft. This season's version of the Heels is void of a go-to low-post player, as James Michael McAdoo has not developed into a player who can take over a game. They also have a freshman point guard in Marcus Paige who is still learning to play at the pace Carolina is accustomed to playing, and as a result, they no longer can simply outscore their opponent.
For the Tar Heels to develop into an elite team they must be tougher and more consistent in their effort and alertness on the defensive end. They need to be tougher off the ball fighting through screens and do a better job communicating. In short, they must take pride in getting stops.
However, I don't see them improving enough on the defensive end to make up for their inexperience and lack of a go-to post player. They are an NCAA tournament team, but not a team that will compete for a national championship. The real remedy for the Tar Heels is one more recruiting class.
Texas Longhorns
It's going to be tough to get a true sense for Texas' abilities this season until they get healthy and the NCAA makes a ruling on Myck Kabongo. Jaylen Bond's health is still an issue, and the NCAA is still holding Kabongo and Texas hostage by not ruling on his eligibility. This is a very young Longhorns team (its top nine players in minutes and points per game are all freshmen or sophomores), and even though Kabongo is only a sophomore himself, he provides coach Rick Barnes with leadership, on-ball defensive toughness and the ability to get in the lane and create easy offense.
This team will improve, but they desperately need a résumé win in the nonconference (a victory over UNC on Wednesday would be a good start). I see a foundation for something special in the future, and there are opportunities on their league schedule to earn quality wins, but without Kabongo and Bond, I don't see a full recovery for Texas until next season.
UCLA Bruins
The Bruins are still trying to develop an identity. They have a talented group of young players that is still learning how to compete each and every play. Although they play hard, there is a difference between playing hard and competing. Playing hard is giving effort, while competing is refusing to give an inch each and every play. One of the hardest things as a coach is to get freshmen to play through mistakes and get to the next play.
In the frontcourt, coach Ben Howland needs more from David and Travis Wear. Both twins are skilled and physically mature and strong, but they must be more productive.
On the perimeter, the Bruins need to find a way to utilize Shabazz Muhammad, Kyle Anderson and their best scorer, Jordan Adams. Anderson struggles defending perimeter players, but is most effective with the ball in his hands, which creates something of a matchup dilemma. Muhammad is an explosive athlete with a high motor, but he is still acclimating to the college game, and Adams is a pure scorer with an old-school game on the offensive end, but he has some defensive deficiencies.
Howland is a terrific man-to-man defensive coach who is being forced to play zone due to his freshmen's deficiencies on the defensive end. This is hurting the Bruins from developing the defense-first identity of Howland's Final Four teams, and offensively, they still play young.
The Bruins will get better, but I do not feel they will improve enough to make the NCAA tournament without winning the Pac-12 tournament.