A note on undefined expression values in programming logics (Q1093365): Difference between revisions
From MaRDI portal
ReferenceBot (talk | contribs) Changed an Item |
Set OpenAlex properties. |
||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1016/0020-0190(87)90158-x / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W1972221707 / rank | |||
Normal rank |
Latest revision as of 11:29, 30 July 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | A note on undefined expression values in programming logics |
scientific article |
Statements
A note on undefined expression values in programming logics (English)
0 references
1987
0 references
In many programming logics, expressions of programming language are used as assertions of the formal system. The problem is that it is normally assumed in mathematical logic that the values of terms and formulas are always defined. This short note describes an approach whose main advantage is that verifications are almost identical to those that can be used when undefinedness cannot occur. The author says that it seems possible to allow undefinedness of expression values in program verification logics without resorting to unfamiliar formal systems, and further it is possible to transform the assertions that arise in the presence of undefinedness into formulas that are almost identical to those conventionally used.
0 references
free logic
0 references
undefinedness
0 references