Content deleted Content added
Line 219:
:The axioms are pretty '''standard''' (at least in the research communities dealing with program correctness), except the names used are typically '''not''' ''get'' and ''set''. Let's take your complaints one by one. (1) Yes, you will need additional axioms to specify ''particular'' types of arrays. These axioms only capture the ''essence'' of an array. (2) Yes, correctness and efficiency are orthogonal issues. (Although there are attempts to analyze efficiency using logic, but they are rather clumsy at the moment.) (3) Yes. Again, they are supposed to be general enough to describe the ''essence'' of what "array" means. (4) No, you are mistaken and I do not see how you reached this conclusion. Finally, regarding your fix: While introducing a special value is certainly possible, note that the current axioms simply ''cannot be applied'' to deduce that something is read from a ___location that was not written, and as such it cannot be proved using this axioms that the read value from an unwritten ___location is constrained in any way. Just Google for "array axioms" and you will find a plethora of resources, pretty much all using the '''same''' axioms. [[User:Rgrig|Rgrig]] ([[User talk:Rgrig|talk]]) 16:58, 10 September 2009 (UTC)
:Also, looking at the history of the article I see that at some point it said that ''I'' stands for a tuple of integers (!!!) and other such nonsensical things. Perhaps it's better it was removed in the end. [[User:Rgrig|Rgrig]] ([[User talk:Rgrig|talk]]) 17:08, 10 September 2009 (UTC)
==Requested move==
| |||