A Generalized Solution for the While Challenge (Extended Abstract)
Sandip Kumar Ray · 2007
Defining a language semantics in ACL2 is tantamount to introducing a function run such that (run stmt st) returns the value of the machine state after executing stmt from state st. The challenge then is to define a function run that formalizes execution of statements in the above language. Young’s expected axiom for run was as follows (where op, arg1, arg2, arg3, run-skip, etc. are suitably defined):