Liste des Groupes | Revenir à theory |
We stipulate that the only measure of a correct emulation is theWhich means the only "correct emulation" that tells the behavior of the program at the input is a non-aborted one.
semantics of the x86 programming language.
_DDD()And thus HHH that do that know only the first N steps of the behavior of DDD, which continues per the definition of the x86 instruction set until the COMPLETE emulation (or direct execution) reaches a terminal instruction.
[00002163] 55 push ebp ; housekeeping
[00002164] 8bec mov ebp,esp ; housekeeping
[00002166] 6863210000 push 00002163 ; push DDD
[0000216b] e853f4ffff call 000015c3 ; call HHH(DDD)
[00002170] 83c404 add esp,+04
[00002173] 5d pop ebp
[00002174] c3 ret
Size in bytes:(0018) [00002174]
When N steps of DDD are emulated by HHH according to the
semantics of the x86 language then N steps are emulated correctly.
When we examine the infinite set of every HHH/DDD pair such that:And thus, the subset that only did a finite number of steps and aborted its emulation on a non-terminal instrucition only have partial knowledge of the behavior of their DDD, and by returning to their caller, they establish that behavior for ALL copies of that HHH, even the one that DDD calls, which shows that DDD will be halting, even though HHH stopped its observation of the input before it gets to that point.
HHH₁ one step of DDD is correctly emulated by HHH.
HHH₂ two steps of DDD are correctly emulated by HHH.
HHH₃ three steps of DDD are correctly emulated by HHH.
...
HHH∞ The emulation of DDD by HHH never stops running.
The above specifies the infinite set of every HHH/DDD pairWrong. EVERY DDD of an HHH that simulated its input for only a finite number of steps WILL halt becuase it will reach its final return.
where 1 to infinity steps of DDD are correctly emulated by HHH.
No DDD instance of each HHH/DDD pair ever reaches past its
own machine address of 0000216b and halts.
Thus each HHH element of the above infinite set of HHH/DDDNope.
pairs is necessarily correct to reject its DDD as non-halting.
Les messages affichés proviennent d'usenet.