Content deleted Content added
rem Move tag |
|||
Line 221:
My idea for fixing the last two bugs was to introduce a "FAIL" value to be the result of accessing an invalid index, and postulate that get(FAIL,I) = set(FAIL,I,V)=FAIL for all I,V; and then remove the phrase "for which the operations are defined". However then the first axiom is violated if ''I'' is an invalid index.<br/>
Does the paper say anythng about these problems? --[[User:Jorge Stolfi|Jorge Stolfi]] ([[User talk:Jorge Stolfi|talk]]) 02:54, 13 May 2009 (UTC)
: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)
==Requested move==
| |||