Relationship between PL and Correctness (5) Checkability Every error should transform a correct program into one whose errors are detectable by the system All error detection based on redundancy(but some forms can cause errors EXamples of userful redundancy type declarations and type checking declarative redundancy variance conditions or assertions Run-time assertions, exception handling hecking subscripts vs array bound case selector vs. case boundsCopyright Nancy Leveson, Sept. 1999 Relationship between PL and Correctness (5) Checkability Every error should transform a correct program into one whose errors are detectable by the system. All error detection based on redundancy (but some forms can cause errors). Examples of userful redundancy: type declarations and type checking declarative redundancy invariance conditions or assertions Run-time assertions, exception handling checking subscripts vs. array bounds case selector vs. case bounds � c