US5748966A
Expired / Lapsed
US
⏱️ 0.0 years remaining
Type error checker for type-free or polymorphic computer language
Assignee: University of Pennsylvania
•
Filing: 1994-12-30
•
Granted: 1998-05-05
•
Expires: 2014-12-30
Abstract
Abstract A system and method for a run-time type error in a program prior to running the program whose source code is written in a programming language with imperative constructs and polymorphic procedures is disclosed. To accomplish the above type error checking, the source code is translated into intermediate form representations by an intermediate form translator. In addition to the intermediate form representations, type representations which include predetermined types such as a locking type constructor and an unlocking type constructor are utilized in detecting the run-time type error. When both intermediate form representations and the type representations are used and the source code is determined to have no run-time type error prior to running the program according to the current invention, it is guaranteed that the program will run without any run-time type error.
Inventors
- 👤 Yoshikazu Sato
Bibliographic Details
Application Number
—
Jurisdiction
US
Data Source
google_patents
Last Synchronized
2026-11-06 20:26
CPC Classifications
G; G06; G06F; G06F8/00; G06F8/40; G06F8/41; G06F8/43; G06F8/436; G06F8/437
Claims Analysis
Total Claims: 67
Claim 1
Independent Claim
166 words
A system for detecting a run-time type error in a program prior to running the program whose source code being written in a programming language with imperative constructs and parametric polymorphic procedures, comprising: an intermediate form translator for translating said source code including imperative constructs and the parametric polymorphic procedures into intermediate form representations; type representations having predetermined types including a locking type constructor and an unlocking type constructor, said locking type constructors locking said predetermined types for defining predetermined locked types so as to ultimately prevent run-time type errors associated with mutuality in relation to said imperative constructs, said unlocking type constructors unlocking said predetermined locked types; and a type checker in response to said intermediate form representations and the type representations for checking whether said predetermined locked types are free of substitution with an exact type so that said program will be free of said run-time type error, said exact type excluding a type equal to and more general than said predetermined locked types.
Claim 2
Independent Claim
166 words
A system for detecting a run-time type error in a program prior to running the program whose source code being written in a programming language with imperative constructs and parametric polymorphic procedures, comprising: an intermediate form translator for translating said source code including imperative constructs and the parametric polymorphic procedures into intermediate form representations; type representations having predetermined types including a locking type constructor and an unlocking type constructor, said locking type constructors locking said predetermined types for defining predetermined locked types so as to ultimately prevent run-time type errors associated with mutuality in relation to said imperative constructs, said unlocking type constructors unlocking said predetermined locked types; and a type checker in response to said intermediate form representations and the type representations for checking whether said predetermined locked types are free of substitution with an exact type so that said program will be free of said run-time type error, said exact type excluding a type equal to and more general than said predetermined locked types.
Claim 3
Dependent Claim
19 words
The system for type checking according to claim 1 wherein said programming language includes at least ML and LISP.
Claim 4
Dependent Claim
33 words
The system for type checking according to claim 2 wherein said polymorphic procedures in said ML are used at least with any combination of constants, term variables, lambda-expressions, function applications and let expressions.
Claim 5
Dependent Claim
24 words
The system for type checking according to claim 1 wherein said mutuality includes a jumping operation with a value passing and a referencing operation.
Claim 6
Dependent Claim
20 words
The system for type checking according to claim 4 wherein said referencing operation further includes reference creation, dereferencing and assignment.
Claim 7
Dependent Claim
30 words
The system for type checking according to claim 1 wherein said predetermined types further include at least a base type, a type variable, a function type, and a reference type.
Claim 8
Dependent Claim
21 words
The system for type checking according to claim 6 wherein said intermediate form representations include expressions, said expressions further including sub-expressions.
Claim 9
Dependent Claim
40 words
The system for type checking according to claim 6 wherein said type checker determines a first type for each of said sub-expressions so as to determine a second type for said expression based upon a plurality of said first types.
Claim 10
Dependent Claim
59 words
The system for type checking according to claim 8 wherein a locked type is provided to a type in said sub-expression when a creation of a mutual object at run time in said sub-expression is detected prior to run time, said locked type being unlocked upon a detection of reference to said mutual object resulting in an unlocked type.
Claim 11
Dependent Claim
27 words
The system for type checking according to claim 9 wherein said mutual object includes a reference cell and a passing value for jumping to a predetermined location.
Claim 12
Dependent Claim
25 words
The system for type checking according to claim 9 wherein said reference includes dereferencing and a use of said passing value in said predetermined location.
Claim 13
Dependent Claim
41 words
The system for type checking according to claim 9 wherein said run-time type error being suspected when said type variable in said locked type defining a locked type variable is substituted with a specific type before resulting in said unlocked type.
Claim 14
Dependent Claim
38 words
The system for type checking according to claim 12 wherein said program is free of said run-time type error when none of said locked type variables is substituted with said specific type before resulting in said unlocked type.
Claim 15
Dependent Claim
26 words
The system for type checking according to claim 13 wherein said specific type excludes a type equal to and more general than said locked type variable.
Claim 16
Dependent Claim
88 words
The system for type checking according to claim 7 wherein said type checker further comparing: a first type checker in response to said intermediate form representations and said type representations for determining a first type for each of said sub-expressions so as to determine a second type for said expression based upon a plurality of said first types; and a second type checker in response to said intermediate form representations and said type representations for further determining if said expression will be free of said run-time type error.
Claim 17
Dependent Claim
24 words
The system for type checking according to claim 15 wherein said first type checker generates a symbol table including local variables and corresponding types.
Claim 18
Dependent Claim
56 words
The system for type checking according to claim 15 wherein a locked type is provided to a type in said sub-expression when a creation of a mutual object at run time in said sub-expression is detected prior to run time, said locked type being marked for unlocking upon a detection of reference to said mutual object.
Claim 19
Dependent Claim
22 words
The system for type checking according to claim 17 wherein said type variable in said locked type defines a locked type variable.
Claim 20
Dependent Claim
46 words
The system for type checking according to claim 18 wherein said first type checker determines a substitution for substituting said locked type variable of a binding expression of said let expression to a specific type, defining at least a part of a let expression typing rule.
Claim 21
Dependent Claim
66 words
The system for type checking according to claim 19 wherein said second type checker in response to said substitution in said first type checker further determines a first type of a local variable of said let expression and then a second type of a body of said let expression based upon said first type indicating that said let expression is free of said run-time type error.
Claim 22
Dependent Claim
42 words
The system for type checking according to claim 20 wherein said let expression typing rule further includes a fork operation and a close operation, a non-locked type variable consisting of none-locked occurrence of a partially locked type variable and not-locked type variable.
Claim 23
Dependent Claim
38 words
The system for type checking according to claim 21 wherein said fork operation replaces each of nonlocked occurrences of said type variables with a fresh type variable except for said non-locked type variable appearing in said symbol table.
Claim 24
Dependent Claim
61 words
The system for type checking according to claim 22 wherein said close operation lists said type variables that may be used for substituting to a specific type, said listed type variables excluding said non-locked type variable appearing in said symbol table, and locked type variables and locked occurrences of partially locked type variables in said first type of said local variable.
Claim 25
Dependent Claim
55 words
The system for type checking according to claim 23 wherein said close operation associates said type variable with said symbol table defining an associated locked type variable if said type variable is not yet associated, fully locked in said first type of said local variable and fully locked or not appearing in said symbol table.
Claim 26
Dependent Claim
29 words
The system for type checking according to claim 24 wherein said type variable has a priority for unification in relation a second type variable based upon said symbol table.
Claim 27
Dependent Claim
30 words
The system for type checking according to claim 25 wherein said second type checker returns said second type of said expression if none of said run-time type error is detected.
Claim 28
Dependent Claim
31 words
The system for type checking according to claim 26 wherein upon a detection of said unlocking constructor at the outer most position in said sub-expression's type, defining an unlocking typing rule.
Claim 29
Dependent Claim
26 words
The system for type checking according to claim 27 wherein said unlocking typing rule further includes an unlock operation, an Ufork operation and said close operation.
Claim 30
Dependent Claim
23 words
The system for type checking according to claim 28 wherein said unlock operation unlocks said marked type which results in an unlocked type.
Claim 31
Dependent Claim
32 words
The system for type checking according to claim 28 wherein said Ufork operation replaces each of said non-locked type variable that is associated with said symbol table with a fresh type variable.
Claim 32
Dependent Claim
40 words
The system for type checking according to claim 25 wherein said associated locked type variable is substituted to said second type variable when said second type variable appears in said symbol table, said unification is defined to be successfully completed.
Claim 33
Dependent Claim
39 words
The system for type checking according to claim 25 wherein said second type variable is substituted to said associated locked type variable when said symbol table lacks said second type variable, said unification is defined to be successfully completed.
Claim 34
Independent Claim
140 words
A method of detecting a run-time type error in a program prior to running the program whose source code being written in a programming language with imperative constructs and parametric polymorphic procedures, comprising the steps of: a. providing type representations hating predetermined types including a locking type constructor and an unlocking type constructor, said locking type constructors locking said predetermined types for preventing run-time type error associated with mutuality in relation to said imperative constructs, said unlocking type constructors unlocking said predetermined locked types; b. translating said source code including imperative constructs and the parametric polymorphic procedures into intermediate form representations; and c. determining in response to said intermediate form representations and said type representations whether said predetermined locked types are free of substitution with an exact type so that said program will be free of said run-time type error.
Claim 35
Independent Claim
140 words
A method of detecting a run-time type error in a program prior to running the program whose source code being written in a programming language with imperative constructs and parametric polymorphic procedures, comprising the steps of: a. providing type representations hating predetermined types including a locking type constructor and an unlocking type constructor, said locking type constructors locking said predetermined types for preventing run-time type error associated with mutuality in relation to said imperative constructs, said unlocking type constructors unlocking said predetermined locked types; b. translating said source code including imperative constructs and the parametric polymorphic procedures into intermediate form representations; and c. determining in response to said intermediate form representations and said type representations whether said predetermined locked types are free of substitution with an exact type so that said program will be free of said run-time type error.
Claim 36
Dependent Claim
19 words
The method of type checking according to claim 33 wherein said programming language includes at least ML and LISP.
Claim 37
Dependent Claim
33 words
The method of type checking according to claim 34 wherein said polymorphic procedures in said ML are used at least with any combination of constants, term variables, lambda-expressions, function applications and let expressions.
Claim 38
Dependent Claim
33 words
The method of type checking according to claim 33 wherein said step c determines whether mutuality in relation to said imperative constricts in said program will be free of said run-time type error.
Claim 39
Dependent Claim
24 words
The method of type checking according to claim 36 wherein said mutuality includes a jumping operation with a value passing and a referencing operation.
Claim 40
Dependent Claim
20 words
The method of type checking according to claim 37 wherein said referencing operation further includes reference creation, dereferencing and assignment.
Claim 41
Dependent Claim
30 words
The method of type checking according to claim 33 wherein said predetermined types further include at least a base type, a type variable, a function type, and a reference type.
Claim 42
Dependent Claim
21 words
The method of type checking according to claim 39 wherein said intermediate form representations include expressions, said expressions further including sub-expressions.
Claim 43
Dependent Claim
40 words
The method of type checking according to claim 40 wherein said step c determines a first type for each of said sub-expressions so as to determine a second type for said expression based upon a plurality of said first types.
Claim 44
Dependent Claim
59 words
The method of type checking according to claim 41 wherein a locked type is provided to a type in said sub-expression when a creation of a mutual object at run time in said sub-expression is detected prior to run time, said locked type being unlocked upon a detection of reference to said mutual object resulting in an unlocked type.
Claim 45
Dependent Claim
27 words
The method of type checking according to claim 42 wherein said mutual object includes a reference cell and a passing value for jumping to a predetermined location.
Claim 46
Dependent Claim
25 words
The method of type checking according to claim 42 wherein said reference includes dereferencing and a use of said passing value in said predetermined location.
Claim 47
Dependent Claim
41 words
The method of type checking according to claim 42 wherein said run-time type error being suspected when said type variable in said locked type defining a locked type variable is substituted with a specific type before resulting in said unlocked type.
Claim 48
Dependent Claim
38 words
The method of type checking according to claim 45 wherein said program is free of said run-time type error when none of said locked type variables is substituted with said specific type before resulting in said unlocked type.
Claim 49
Dependent Claim
26 words
The method of type checking according to claim 46 wherein said specific type excludes a type equal to and more general than said locked type variable.
Claim 50
Dependent Claim
82 words
The method of type checking according to claim 40 wherein said step c further comprises the steps of: d. determining a first type for each of said sub-expressions in response to said intermediate form representations and said type representations and then a second type for said expression based upon a plurality of said first types; and e. further determining in response to said intermediate form representations and said type representations whether if said expression will be free of said run-time type error.
Claim 51
Dependent Claim
23 words
The method of type checking according to claim 48 wherein said step d generates a symbol table including local variables and corresponding types.
Claim 52
Dependent Claim
56 words
The method of type checking according to claim 48 wherein a locked type is provided to a type in said sub-expression when a creation of a mutual object at run time in said sub-expression is detected prior to run time, said locked type being marked for unlocking upon a detection of reference to said mutual object.
Claim 53
Dependent Claim
22 words
The method of type checking according to claim 50 wherein said type variable in said locked type defines a locked type variable.
Claim 54
Dependent Claim
45 words
The method of type checking according to claim 51 wherein said step d determines a substitution for substituting said locked type variable of a binding expression of said let expression to a specific type, defining at least a part of a let expression typing rule.
Claim 55
Dependent Claim
65 words
The method of type checking according to claim 52 wherein said step e in response to said substitution in said first type checker further determines a first type of a local variable of said let expression and then a second type of a body of said let expression based upon said first type indicating that said let expression is free of said run-time type error.
Claim 56
Dependent Claim
42 words
The method of type checking according to claim 53 wherein said let expression typing rule further includes a fork operation and a close operation, a non-locked type variable consisting of none-locked occurrence of a partially locked type variable and not-locked type variable.
Claim 57
Dependent Claim
38 words
The method of type checking according to claim 54 wherein said fork operation replaces each of nonlocked occurrences of said type variables with a fresh type variable except for said non-locked type variable appearing in said symbol table.
Claim 58
Dependent Claim
61 words
The method of type checking according to claim 55 wherein said close operation lists said type variables that may be used for substituting to a specific type, said listed type variables excluding said non-locked type variable appearing in said symbol table, and locked type variables and locked occurrences of partially locked type variables in said first type of said local variable.
Claim 59
Dependent Claim
55 words
The method of type checking according to claim 56 wherein said close operation associates said type variable with said symbol table defining an associated locked type variable if said type variable is not yet associated, fully locked in said first type of said local variable and fully locked or not appearing in said symbol table.
Claim 60
Dependent Claim
29 words
The method of type checking according to claim 57 wherein said type variable has a priority for unification in relation a second type variable based upon said symbol table.
Claim 61
Dependent Claim
29 words
The method of type checking according to claim 58 wherein said step e returns said second type of said expression if none of said run-time type error is detected.
Claim 62
Dependent Claim
31 words
The method of type checking according to claim 59 wherein upon a detection of said unlocking constractor at the outer most position in said sub-expression's type, defining an unlocking typing rule.
Claim 63
Dependent Claim
26 words
The method of type checking according to claim 60 wherein said unlocking typing rule further includes an unlock operation, an Ufork operation and said close operation.
Claim 64
Dependent Claim
23 words
The method of type checking according to claim 61 wherein said unlock operation unlocks said marked type which results in an unlocked type.
Claim 65
Dependent Claim
32 words
The method of type checking according to claim 61 wherein said Ufork operation replaces each of said non-locked type variable that is associated with said symbol table with a fresh type variable.
Claim 66
Dependent Claim
40 words
The method of type checking according to claim 58 wherein said associated locked type variable is substituted to said second type variable when said second type variable appears in said symbol table, said unification is defined to be successfully completed.
Claim 67
Dependent Claim
39 words
The method of type checking according to claim 58 wherein said second type variable is substituted to said associated locked type variable when said symbol table lacks said second type variable, said unification is defined to be successfully completed.
References Cited (Backward Citations)
USPTO Annuity & Maintenance Windows
| Annuity Stage | Window Opens | Payment Deadline | Surcharge Period Until | Estimated Fee | Status |
|---|---|---|---|---|---|
| 3.5 Years (Year 4) | 2001-05-04 | 2001-11-03 | 2002-05-05 | $2000.00 | Window Closed / Lapsed |
| 7.5 Years (Year 8) | 2005-05-04 | 2005-11-03 | 2006-05-05 | $3760.00 | Window Closed / Lapsed |
| 11.5 Years (Year 12) | 2009-05-04 | 2009-11-03 | 2010-05-05 | $7700.00 | Window Closed / Lapsed |