3

As someone somewhat familiar with termination analysis, I'd say that the techniques are only as ad-hoc as the programs they aim to prove termination of, which is to say very ad-hoc indeed. The crucial approach to scaling such analyses is modularity which allows decomposing the problem into sub-problems. Indeed this usually consists in identifying cycle-like ...


1

Firstly, in addition to the Standard from 2002, there is also Technical Corrigendum 1 (TC1) from 2007 which fixes a number of issues. I don't know of any combined document. Both documents are available free of charge and links to them are available on the Z notation Wikipedia page. However, for this particular question, TC1 is not relevant. Section 15 ...


Only top voted, non community-wiki answers of a minimum length are eligible