| 
|
Group: type checking
topics >
computer science >
compiler error checking
Topic:
constraints
Topic:
data type compatibility
Topic:
dependency analysis
Topic:
dynamic type checking
Topic:
flavor analysis and typestates for supplementary type checking
Topic:
range checking
Topic:
run-time assertions
Topic:
self-identifying data structures
Topic:
type checking by trademark
Topic:
type-safe and secure languages
Topic:
weak vs. strong type checking
data type
Group:
parameters
Group:
program proving
Group:
security
Group:
software maintenance
Group:
testing
Topic:
consistency testing
Topic:
dynamic vs. static data type
Topic:
error safe systems
Topic:
function syntax definition
Topic:
path expression
Topic:
preventing accidental errors
Topic:
structural equivalence vs. name equivalence of data types
Topic:
type reflection and introspection
Topic:
type-safe and secure languages
Topic:
units
Topic:
XML schemas
Summary
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: data type rules
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: representation independence
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: type checking XML
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: nonsensical execution, unintended interpretation
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: data type as error detection
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: type field
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: implementation of type checking
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: limitations of type systems
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]
Quote: type systems say nothing about concurrency or dynamics; e.g., that initialize happens first, or x() must be invoked every 10 ms
[»leeEA9_2000]
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)
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)