Termination Assertions for Recursive Programs: Completeness and Axiomatic Definability
The termination assertion p<S>q means that whenever the formular p is true, there is an execution of the possibly nondeterministic program S which terminates in a state in qhich q is true. A recursive program S may declare and use local variables and nondeterministic recursive procedures with...
| Main Authors: | , |
|---|---|
| Published: |
2023
|
| Online Access: | https://hdl.handle.net/1721.1/149024 |