home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1993 #3 / NN_1993_3.iso / spool / comp / theory / 2916 < prev    next >
Encoding:
Internet Message Format  |  1993-01-23  |  2.0 KB
  1. Path: sparky!uunet!mcsun!uknet!mucs!cliff
  2. From: cliff@cs.man.ac.uk (Cliff B Jones)
  3. Newsgroups: comp.theory
  4. Subject: History
  5. Message-ID: <1993Jan22.172329@cs.man.ac.uk>
  6. Date: 22 Jan 93 17:23:29 GMT
  7. Sender: news@cs.man.ac.uk
  8. Organization: Dept Computer Science, University of Manchester, U.K.
  9. Lines: 58
  10.  
  11. A Technical Report (details below) containing references to papers of
  12. historical interest in the area of `formal methods' is available
  13. either by FTP from
  14.  
  15.             m1.cs.man.ac.uk (130.88.13.4)
  16.  
  17.         pub/TR/umcs-92-12-2.ps.Z
  18.  
  19. or in hard copy by e-mailing
  20.  
  21.             jenny@cs.man.ac.uk
  22.  
  23. +++++++++++++++++++++++++++++++++++++++++++++++++++++++
  24.  
  25. Formal Methods -- Selected Historical References
  26.  
  27. C. B. Jones and A. M. McCauley
  28.     Department of Computer Science
  29.     University of Manchester
  30.     Oxford Rd., Manchester, U.K.
  31.  
  32. \date{1992-12-09}
  33.  
  34. Abstract
  35.  
  36. This report contains citations to papers which are of
  37. historical interest in the area of formal approaches
  38. to software development. 
  39.  
  40. +++++++++++++++++++++++++++++++++++++++++++++++++++++++
  41. +++++++++++++++++++++++++++++++++++++++++++++++++++++++
  42.  
  43. Also available in hard copy (no ftp for copyright reasons) is
  44.  
  45. +++++++++++++++++++++++++++++++++++++++++++++++++++++++
  46. The Search for Tractable Ways of Reasoning about Programs
  47.  
  48. C.\ B.\ Jones
  49.  
  50. \date{1992-03-31 (minor typographical errors corrected: 1992-06-23)}
  51.  
  52. Abstract
  53.  
  54. This paper traces the most important steps in the history of research
  55. on reasoning about programs.
  56. The main focus is on ways of verifying that sequential imperative
  57. programs satisfy their specifications.
  58. Over time it has become clear that {\em post facto} verification is
  59. only practical for small programs;
  60. verification methods which support the development of larger programs
  61. exploit a notation of compositionality.
  62. Coping with concurrent algorithms is much more challenging --
  63. this and other extensions are considered briefly.
  64. The main thesis is that the idea of reasoning about programs has been
  65. around for a long time;
  66. the search has been to find tractable methods.
  67.  
  68. +++++++++++++++++++++++++++++++++++++++++++++++++++++++
  69.