home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1993 #1 / NN_1993_1.iso / spool / comp / specific / 600 next >
Encoding:
Internet Message Format  |  1993-01-04  |  2.4 KB
  1. Path: sparky!uunet!olivea!decwrl!src.dec.com!src.dec.com!jmason
  2. From: src-report@src.dec.com (James Mason)
  3. Newsgroups: comp.specification
  4. Subject: Publication announcement on Larch research paper
  5. Message-ID: <1993Jan4.205832.19967@src.dec.com>
  6. Date: 4 Jan 93 20:58:32 GMT
  7. Sender: jmason@src.dec.com (James Mason)
  8. Organization: DEC Systems Research Center
  9. Lines: 54
  10.  
  11.  
  12.  
  13.             PUBLICATION ANNOUNCEMENT
  14.             ------------------------    
  15.               
  16.         DIGITAL SYSTEMS RESEARCH CENTER
  17.         -------------------------------
  18.  
  19. Below is an abstract of a newly available SRC Research Report. 
  20.  
  21. You can retrieve it via anonymous ftp from gatekeeper.pa.dec.com. The
  22. pathname to it is: /pub/DEC/SRC/research-reports/
  23. Please read the README file before retrieving.
  24.  
  25. The report is also retrievalbe via DECnet and VMS in the following directory:
  26. DECWRL::"/pub/DEC/SRC/research-reports"
  27. i.e. type at the prompt> dir decwrl::"/pub/DEC/SRC/research-reports"
  28.  
  29.  
  30.  
  31.  
  32. "Experiences with Software Specification and Verification Using LP, the
  33. Larch Proof Assistant"
  34. Manfred Broy
  35. Report #93, November 12, 1992
  36.  
  37. 69 pages
  38.  
  39.  
  40. Author's abstract: 
  41.  
  42. We sketch a method for deduction-oriented software and system development
  43. The method incorporates formal machine-supported specification and 
  44. verification as activities in software and systems development. We
  45. describe experiences in applying this method. These experiences have
  46. been gained by using the LP, the Larch proof assistant, as a tool for 
  47. a number of small and medium size case studies for the formal development 
  48. of software and systems. LP is used for the verification of the
  49. development steps. These case studies include
  50.  
  51.     * quicksort
  52.     * the majority vote problem
  53.     * code generation by a compiler and its correctness
  54.     * an interactive queue and its refinement into a network
  55.  
  56. The developments range over levels of requirement specifications, designs 
  57. and abstract implementations. The main issues are questions of a
  58. development method and how to make good use of a formal tool like LP in
  59. a goal-directed  way within the development. We further discuss of the 
  60. value of advanced specification techniques, most of which are deliberately 
  61. not supported by LP and its notation, and their significance in development.
  62. Furthermore, we discuss issues of enhancement of a support system like
  63. LP and the value and the practicability of using formal techniques such 
  64. as specification and verification in the development process in practice.
  65.