Group: type checking

topics > computer science > Group: data

compiler error checking
data type compatibility
dependency analysis
dynamic type checking
flavor analysis and typestates for supplementary type checking
range checking
run-time assertions
self-identifying data structures
type checking by trademark
type-safe and secure languages
weak vs. strong type checking
data type
program proving
software maintenance

consistency testing
dynamic vs. static data type
error safe systems
function syntax definition
path expression
preventing accidental errors
structural equivalence vs. name equivalence of data types
type reflection and introspection
type-safe and secure languages
XML schemas


Type checking is an effective compile-time error test for program consistency. Argument types must match parameter types and the left hand side of a replace must match the type of the right hand side. Limited type conversions may be allowed. If properly defined, type checking can guarantee representational independence. Run-time type checking may perform additional range checks on array indices. (cbb 5/80)

Type checking is a simple formal verification of a program. If operand types do not match, execution would be nonsensical. For example, nonsensical results are produced by the integer addition of floating-point numbers. Compatible types may be freely substituted. If a type defines an interface, than any implementation of the interface may be used.

Type systems define the type name for each entity. They check assignments, initializations, and invocations for type compatibility. One type may be a subtype of another, or convert to another type.

At run-time, a program may validate types, parameters, input, and results. Is this a valid array index? Does this XML document conform to its schema? Is this value an instance of a database domain? Does this object obey its type invariants? How is this type serialized; how is it unambiguously erased to an untyped representation?

Type annotations, flow analysis, and model checking can identify usage errors and concurrency errors. (cbb 7/06)

Subtopic: formal type checking up

Quote: use spi calculus for typechecking security protocols using shared-key cryptography [»abadM9_1999]
Quote: predicate dispatch invokes a method only if a predicate is true; JPred uses decision procedures for dispatch and type checking; based on Cooperating Validity Checker (CVC) [»millT10_2004]

Subtopic: data type rules up

Quote: a type is a subtype if every value matches the base type; because of named element typing, verify by regular expressions [»simeJ1_2003]
Quote: type T is assignable to type U if it is a subtype, an array supertype, a reference supertype, or an overlapping ordinal type [»cardL_1991]
Quote: an expression is assignable to a variable if their types are assignable, the value is valid, not a local procedure, nor an array of a different shape

Subtopic: representation independence up

Quote: type checking in Russell guarantees representation independent semantics [»demeA_1978]
Quote: two arguments have the same type if both name the same mathematical domain [»harmDE5_1991]
Quote: mathematical definitions of types as extensional sets miss the importance of type checking [»morrJH10_1973]
Quote: a standard stream package for Modula-3; illustrates partially opaque types and the isolation of unsafe code; based on Topaz [»browMR_1991]

Subtopic: type checking XML up

Quote: instead of matching, an XML value validates against a type; either produces an internal value or it fails; e.g., element ints of type intsType { 1, 2, 3 } [»simeJ1_2003]
Quote: validation theorem -- validates iff matches and erases; roundtripping if unambiguous [»simeJ1_2003]
Quote: a validated element must match its type, since validation yields sensible values; consequence of pure named typing [»simeJ1_2003]

Subtopic: nonsensical execution, unintended interpretation up

Quote: system programmers sees types as protection of bit strings from unintended interpretation [»wegnP10_1986]
Quote: it is hard for a program to guarantee uniqueness, data type consistency, and initialization [»stroB_1994]
Quote: nonsensical execution causes arbitrary damage; may not effect program behavior until much later [»stroRE1_1986]
Quote: a programming system should detect all programs that violate its definition or intended structure [»maclBJ_1987]
Quote: type checking ensures well-defined operations on data; security checking ensures authorization to execute operations [»brinP_1973]

Subtopic: data type as error detection up

Quote: type consistency should be checked as soon as sufficient information is available; unifies static and dynamic typing [»heerJ4_1985]
Quote: type checking of function calls reduces duration of interface errors and frequency of interface defects; good experimental design [»precL4_1998]
Quote: type checking can catch inappropriate indexing of arrays; like units; e.g., ArrayIndex h, ColumnIndex i, and RowIndex j [»weihK9_2002]
Quote: type checking catches errors which are independent of the context of an operation relative to other operations [»stroRE1_1986]
Quote: errors should be checked at multiple levels to ensure that all errors are caught somewhere [»maclBJ_1987]
Quote: type systems do more than any other formal method to ensure correctness; constrains interface; ensures compatibility [»leeEA9_2000]
Quote: the required category of an ML word must match the actual category of its sub-domain [»spooCR4_1986]
Quote: type checking authenticates valid types prior to processing and keeps secret the procedures that implement the type [»morrJH10_1973]

Subtopic: type field up

Quote: a type field leads to two kinds of errors in large programs: failure to test the type field and missed cases in a switch [»stroB_1991]

Subtopic: implementation of type checking up

Quote: type checking normally occurs with the abstract syntax tree; allows context, type correctness of subexpressions, and one type rule per construct [»deanD5_1996]
Quote: a bytecode verifier must show that all possible execution paths have the same virtual machine configuration; complicates type checking
Quote: SafeTSA assigns a separate register plane for every type; guarantees type separation without type and range checks [»ammeW6_2001]

Subtopic: limitations of type systems up

Quote: type systems say nothing about concurrency or dynamics; e.g., that initialize happens first, or x() must be invoked every 10 ms

Group: type checking up

Topic: compiler error checking (16 items)
Topic: constraints (35 items)
Topic: data type compatibility (5 items)
Topic: dependency analysis (34 items)
Topic: dynamic type checking (43 items)
Topic: flavor analysis and typestates for supplementary type checking (68 items)
Topic: range checking (20 items)
Topic: run-time assertions (25 items)
Topic: self-identifying data structures (18 items)
Topic: type checking by trademark (13 items)
Topic: type-safe and secure languages (43 items)
Topic: weak vs. strong type checking
(42 items)

Related Topics up

Group: data type   (34 topics, 730 quotes)
Group: parameters   (10 topics, 145 quotes)
Group: program proving   (10 topics, 311 quotes)
Group: security   (23 topics, 874 quotes)
Group: software maintenance   (14 topics, 368 quotes)
Group: testing   (18 topics, 557 quotes)

Topic: consistency testing (60 items)
Topic: dynamic vs. static data type (24 items)
Topic: error safe systems (76 items)
Topic: function syntax definition (17 items)
Topic: path expression (14 items)
Topic: preventing accidental errors (37 items)
Topic: structural equivalence vs. name equivalence of data types (30 items)
Topic: type reflection and introspection (28 items)
Topic: type-safe and secure languages (43 items)
Topic: units (23 items)
Topic: XML schemas
(16 items)

Updated barberCB 6/05
Copyright © 2002-2008 by C. Bradford Barber. All rights reserved.
Thesa is a trademark of C. Bradford Barber.