Title:
|
Intermittent-assertion method as a structural induction (English) |
Author:
|
Vosátka, Karel |
Language:
|
English |
Journal:
|
Kybernetika |
ISSN:
|
0023-5954 |
Volume:
|
15 |
Issue:
|
2 |
Year:
|
1979 |
Pages:
|
(122)-135 |
. |
Category:
|
math |
. |
MSC:
|
68B10 |
MSC:
|
68Q60 |
idZBL:
|
Zbl 0399.68021 |
idMR:
|
MR542057 |
. |
Date available:
|
2009-09-24T17:06:39Z |
Last updated:
|
2012-06-05 |
Stable URL:
|
http://hdl.handle.net/10338.dmlcz/124478 |
. |
Reference:
|
[1] R. M. Burstall: Program Proving as Hand Simulation with a Little Induction.Information Processing 74, North-Holland Publ. Comp., 1974, 308-312. Zbl 0299.68012, MR 0448980 |
Reference:
|
[2] Z. Manna R. Waldinger: Is "sometime" sometimes better than "always"? Intermittent assertions in proving program correctness.Stanford Artif. Intel. Lab. STAN-CS-76-558, June 1976 (also in CACM 21 (1978), 2, 159-179). MR 0483642 |
Reference:
|
[3] R. W. Floyd: Assigning meanings to programs.Proceedings of Symposium in Applied Math., American Math. Soc. 1967, 19-32. Zbl 0189.50204, MR 0235771 |
Reference:
|
[4] J. H. Morris, Jr., Ben Wegbreit: Subgoal induction.CACM 20 (1977), 4, 209-220. MR 0445889 |
Reference:
|
[5] R. M. Burstall: Proving properties of programs by structural induction.The Comp. Jour. 12 (1969), 1,41-48. Zbl 0164.46202 |
Reference:
|
[6] Z. Manna: Mathematical Theory of Computation.McGrow-Hill Book Comp., New York 1974. Zbl 0353.68066, MR 0400771 |
Reference:
|
[7] C. Reynolds R. T. Yeh: Induction as the basis for program verification.IEEE Tran. on Software Engineering SE-2 (1976), 4, 244-252. MR 0520721 |
. |