Les modalités de la correction totale

Luis Fariñas Del Cerro

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications (1982)

  • Volume: 16, Issue: 4, page 349-363
  • ISSN: 0988-3754

How to cite


Fariñas Del Cerro, Luis. "Les modalités de la correction totale." RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 16.4 (1982): 349-363. <http://eudml.org/doc/92170>.

author = {Fariñas Del Cerro, Luis},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications},
keywords = {termination of programs; modal formulas; propositional modal logic; invariance; eventuality; temporal operators; automatic theorem-proving},
language = {fre},
number = {4},
pages = {349-363},
publisher = {EDP-Sciences},
title = {Les modalités de la correction totale},
url = {http://eudml.org/doc/92170},
volume = {16},
year = {1982},

AU - Fariñas Del Cerro, Luis
TI - Les modalités de la correction totale
JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY - 1982
PB - EDP-Sciences
VL - 16
IS - 4
SP - 349
EP - 363
LA - fre
KW - termination of programs; modal formulas; propositional modal logic; invariance; eventuality; temporal operators; automatic theorem-proving
UR - http://eudml.org/doc/92170
ER -


  1. [AW1] E. ASHCROFTet W. WADGE, Lucid, a Non Procedural Language with Iteration, Com. A.C.M., vol. 20, n° 7, July 1977, p. 519-526. Zbl0358.68033
  2. [AW2] E. ASHCROFTet W. WADGE, Intermittent Assertion Proofs in Lucid, I.F.I.P. 77, p. 723-726. Zbl0363.68021MR474941
  3. [B] BURSTALL, Program Proving as Hand Simulation with a Little Induction, I.F.I.P. 74, p. 308-312. Zbl0299.68012MR448980
  4. [C] R. CARNAP, Modalities and Quantification, J.S.L., vol. 11, n° 2, 1946, p. 33-64. Zbl0063.00713MR19562
  5. [E] E. ENGELER, Algoritmic Properties of Structures, Math. Sys. The., vol. 1, n° 3, p. 183-185. Zbl0202.00802MR224473
  6. [EP] P. ENJALBERT, Systèmes de déduction pour les arbres et les schémas de programmes, R.A.I.R.O. Inform. Théor., vol. 14, n° 3, 1980, p. 247-278. Zbl0441.68007MR593490
  7. [F] FARIÑAS DEL CERRO, Un principe de résolution en logique modale (à paraître). Zbl0566.03007
  8. [FL] FLOYD, Assigning Meaning to Programs, Proc. Amer. Math. Soc. Symp. in App. Math., vol. 19, 1967, p. 19-31. Zbl0189.50204MR235771
  9. [H] D. HAREL, First-Order Dynamic Logic, Lectures Notes in Computer Science, Springer Verlag, n° 68. Zbl0403.03024MR567695
  10. [HKP] HAREL, KOZEN et PARIKH, Process Logic, Expressiveness, Decidebility, Completeness, F.O.C.S. 80, p. 129-142. MR596055
  11. [HO] HOARE, An Axiomatic Basic of Computer Programming, Com. A.C. M., vol.12, n° 10, 1969. Zbl0179.23105
  12. [HC] HUGHES et CRESSWELL, An Introduction to Modal Logic, Mathuem et Co., London, 1978. Zbl0205.00503
  13. [K] KRÖGER, LAR: A Logic for Algohthmic Reasoning, Acta Informatica, 1977, p. 243-266. Zbl0347.68016
  14. [Ml] Z. MANNA, Properties of Programs and First Order Predicate Calculus, J.A.C.M., vol. 16, n° 2, 1969, p. 244-255. Zbl0198.22001
  15. [M2] Z. MANNA, Logics of Programs, Proc, I.F.I.P. 80, North-Holland, p, 41-52. 
  16. [MP] Z. MANNAet A. PNUELI, The Modal Logic of Programs, Memo AIM-330 Stanford A.I. Laboratory, Sept. 1979. 
  17. [NW] Z. MANNAet R. WALDINGER, Is "sometime" sometime better than "always"?: Intermittent Assertions in Proving Program Correcteness, Com. A.C.M., vol. 21, n° 2, 1978, p. 159-172. Zbl0367.68011MR483642
  18. [Mc] MCARTHUR, Tense Logic, Reidel Publ., 1976. Zbl0371.02013MR536334
  19. [MCT] MCKINSEY, et TARSKI, Some Theorems about the Sentential Calculi of Lewis and Heyting, J.S.L., vol. 13, 1948, p. 1-15. Zbl0037.29409MR24396
  20. [MI] MINC, Communication personnelle. 
  21. [0] ORLOWSKA, Resolution Systems and their Applications, I, II Fundamenta Informaticae, p. 235-267, p. 333-362. Zbl0472.68052MR591776
  22. [P] W. T. PARRY, Modalities in the Survey System of Strict Implication, J.S.L., vol. 4, 1939, p. 131-154. Zbl0023.09902JFM65.1105.04
  23. [PR] V. R. PRATT, Semantical Considerations on Floyd-Hoare Logic, Proc. 17th Ann. I.E.E.E. Symp. on Foundations of Comp. Sc., 1976, p. 109-121. MR502164
  24. [RS] RASIOWA et SIKORSKI, The Mathematics of Metamathematics, Warszowa, 1963. Zbl0122.24311
  25. [R] ROBINSON, A Machine Oriented Logic Based on the Resolution Principle, J.A.C.M., vol.12, 1965, p. 23-41. Zbl0139.12303MR170494
  26. [S] SALWICKI, Formatized Algorithme Language, Bull. Ac. Pol. Sc., vol. 18, n° 5, 1970, p. 227-232. Zbl0198.02801MR270852
  27. [VE] M. VAN EMDEN, Verification Conditions as Programs, Automate Languages and Programming, MICHEALSON and MILNER, éd., Edinburg Univ. Press, 1976, p. 99-119. Zbl0403.68015

NotesEmbed ?


You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.


Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.