boolean terminate (void *p); /* * Precondition: p is a pointer to a parameter-free function * Postcondition: return true if and only if (*p) () terminates * Property: terminate (*p) terminates on any input p */
We are going to show that such a terminating terminate() function cannot exist. (Note that if such a function cannot exist for parameter-free functions, then it cannot exist at all for more general functions, since general functions include parameter-free functions.) To this aim, we define the following four functions skip(), loop(), loop_if_terminate(), and self_loop_if_terminate():
void skip () {} /* do nothing and terminate */
void loop () { for ( ; ; ); } /* do nothing and never terminate */
boolean loop_if_terminate (void *p) { boolean b = terminate (p); if (b) loop (); else return b; }
boolean self_loop_if_terminate () { return loop_if_terminate (&self_loop_if_terminate); }
boolean f01 () { return terminate (&loop); } boolean f02 () { return terminate (&skip); } boolean f03 () { return loop_if_terminate (&loop); } boolean f04 () { return loop_if_terminate (&skip); } boolean f05 () { return terminate (&f01); } boolean f06 () { return terminate (&f02); } boolean f07 () { return terminate (&f03); } boolean f08 () { return terminate (&f04); } boolean f09 () { return loop_if_terminate (&f01); } boolean f10 () { return loop_if_terminate (&f02); } boolean f11 () { return loop_if_terminate (&f03); } boolean f12 () { return loop_if_terminate (&f04); }