home *** CD-ROM | disk | FTP | other *** search
/ ftp.umcs.maine.edu / 2015-02-07.ftp.umcs.maine.edu.tar / ftp.umcs.maine.edu / pub / WISR / wisr5 / proceedings / ascii / mili_a.ascii < prev    next >
Text File  |  1993-05-31  |  14KB  |  318 lines
  1.  
  2. A Formal Approach to Software Reuse:  Design and Implementation 
  3.  
  4. Ali Mili, Rym Mili 
  5.  
  6. Department of Computer Science 
  7. University of Ottawa, Ottawa, Ont. K1N 6N5, Canada 
  8. Tel: (613) 564-9234, fax: (613) 564-5045 
  9. Email: (amili, rmili)@csi.uottawa.ca 
  10.  
  11. Roland T. Mittermeir 
  12.  
  13. Instit  f  Informatik 
  14. Universit  Klagenfurt, A-9022 Klagenfurt Austria 
  15. Tel: (43-463) 2700575, fax (43-463) 2700505 
  16. Email: roland@samos.ifi.uni-klu.ac.at 
  17.  
  18.  
  19.                           Abstract  
  20.  
  21. Formal specifications and program correctness concepts are widely
  22. recognized as effective in dealing with the richness and complexity
  23. of software components.  In this paper we submit the position that
  24. these concepts can be put to bear on the problem of maintaining a
  25. database of software components for the purpose of reusing them. To
  26. support our claim, we discuss a system we are currently designing for
  27. this purpose.  A first prototype of this system is written in Prolog
  28. and contains a toy database.  A full size version of the system is
  29. being designed by means of a theorem prover named Otter 2.2 (copyright 
  30. Argonne National Laboratory).
  31.  
  32. Keywords:  formal specification, program correctness, theorem proving, 
  33.        software reuse, software archive.
  34.  
  35. Workshop Goals:  Learning; networking; gaining a feel of how our effort fits in
  36.                  the global research effort; identifying fields where our 
  37.          contribution will be most useful; fine-tuning our design 
  38.          orientations.
  39.  
  40. Working Groups:  reuse and formal methods, tools and environments, reuse 
  41.          process models.
  42.  
  43.  
  44. 1  Background 
  45.  
  46. The approach advocated in this paper results from the combination of two 
  47. research efforts:
  48.   
  49.   1. An effort by the third author to build a software archive as a stratified 
  50.      multidimensional classification structure for software components.
  51.  
  52.   2. An effort by the first author (and more recently the second) to 
  53.      investigate various features of the specification process and the 
  54.      specification product.
  55.   
  56.  
  57. In a recent joint publication [NBM92] the first and third authors make a 
  58. proposal for constructing a database of software components, based on the 
  59. following premises:
  60.   
  61.   * Entries of the database have the form of (specification, program) pairs, 
  62.     where the program component is correct with respect to the specification 
  63.     component.
  64.  
  65.   * The set of database entries is [NBM92] by means of an ordering relation 
  66.     among specifications, whose interpretation is: a specification S1 is greater
  67.     than a specification S2 if and only if any program correct with respect to 
  68.     S1 is correct with respect to S2.  This is called the refinement ordering.
  69.  
  70.   * The retrieve key for retrieval operations on the database take the form of a
  71.     specification, and seek to determine all the programs of the database that 
  72.     are correct with respect to the key, by matching the key against the 
  73.     specification components of database entries.
  74.   
  75.  
  76. Our design rationale is that by representing database entries with arbitrarily 
  77. abstract specifications and by letting the match between a store key and a 
  78. retrieve key be defined by the refinement ordering (rather than strict 
  79. equality), we deal effectively with the diversity of software components and the
  80. complexity of organizing such components in a database.
  81.  
  82. In this position paper we give a brief progress report of our effort to build 
  83. this database, then we compare our effort with others.
  84.  
  85.  
  86. 2  Position 
  87.  
  88. 2.1  A Database Structure 
  89.  
  90. In order to illustrate the structure that we propose for a database of software
  91. components, we present an example with eight specifications and eight programs.
  92. This example is used in the Prolog-based first prototype of our system.
  93.  
  94. The specifications are defined as binary relations on the set 
  95. S = 0, 1, 2, 3, 4, 5, 6, 7, 8.
  96.  
  97.     R0 = 0
  98.  
  99.     R1 = (s1,s2) OR s2 mod 2 = 0 AND s2 <= s1 + 1. 
  100.  
  101.     R2 = (s1,s2) OR s1 mod 2 = 0 AND s2 >= s1. 
  102.  
  103.     R3 = (s1,s2) OR s1 mod 2 = 1 AND s2 >= s1 + 1. 
  104.  
  105.     R4 = (s1,s2) OR s1 mod 2 = 0 AND s2 >= s1 UNION
  106.          (s1,s2) OR s1 mod 2 = 1 AND s2 mod 2 = 0 AND s2 <= s1 + 1. 
  107.  
  108.     R5 = (s1,s2) OR s1 mod 2 = 1 AND s2 = s1 + 1 UNION
  109.          (s1,s2) OR s1 mod 2 = 0 AND s2 mod 2 = 0 AND s2 <= s1 + 1. 
  110.  
  111.     R6 = (s1,s2) OR s1 mod 2 = 0 AND s2 >= s1 UNION
  112.          (s1,s2) OR s1 mod 2 = 1 AND s2 >= s1 + 1. 
  113.  
  114.     R7 = (s1,s2) OR s1 mod 2 = 0 AND s2 = s1 UNION
  115.          (s1,s2) OR s1 mod 2 = 1 AND s2 = s1 + 1. 
  116.  
  117.  
  118. The programs are defined by begin-end blocks written in Pascal's syntax on an 
  119. integer variable s. 
  120.  
  121.     p0: begin s := 5 end. 
  122.     p1: begin s := 0 end. 
  123.     p2: begin end. 
  124.     p3: begin s := s + 1 end. 
  125.     p4: begin if s mod 2 = 1 then s := 0 end. 
  126.     p5: begin if s mod 2 = 0 then s := 0 else s := s + 5 end. 
  127.     p6: begin if s mod 2 = 1 then s := s + 5 end. 
  128.     p7: begin if s mod 2 = 1 then s := s + 1 end. 
  129.  
  130.  
  131. Once we arrange the specifications according to the refinement ordering relation
  132. and attach the appropriate specifications to programs, we obtain the structure 
  133. described in figure 1.
  134.  
  135.                        R7 * p7
  136.                          /|\
  137.                         / | \
  138.                        /  |  \
  139.                       /   |   \
  140.                      / R6 * p6 \ 
  141.                     /    / \    \ 
  142.                    /    /   \    \
  143.                   /    /     \    \
  144.                  /    /       \    \
  145.                 /    /         \    \
  146.             R5 * p5 /           \ R4 * p4
  147.                |\  /             \  /|
  148.                | \/               \/ | 
  149.                | /\               /\ |
  150.                |/  \             /  \|
  151.             R3 * p3 \           / R2 * p2
  152.                 \    \         /    /
  153.                  \    \       /    /
  154.                   \    \     /    /
  155.                    \    \   /    /
  156.                     \    \ /    /
  157.                      \ R1 * p1 /
  158.                       \   |   /
  159.                        \  |  /
  160.                         \ | /
  161.                          \|/
  162.                        R0 * p0
  163.  
  164.     Figure 1:  A Database of Software Components 
  165.  
  166.  
  167. A number of storage and retrieval algorithms have been defined on this database
  168. structure. These are essentially graph manipulation and traversal algorithms.  
  169. The details of these algorithms are given in [NBM92].
  170.  
  171.  
  172. 2.2  Implementation Options 
  173.  
  174. The database presented in figure 1 is implemented in Prolog as a first prototype
  175. of our system.  Prolog is adequate for this simple example, where specifications
  176. are finite and their representation is simple, but is not sufficiently powerful
  177. for general specifications, that are arbitrarily complex and are represented in 
  178. arbitrarily abstract terms.  Hence for the full size system we are relying on a
  179. theorem prover to carry out the comparisons between store keys and retrieve 
  180. keys.
  181.  
  182. A typical application of the theorem prover we are using for our purposes is the
  183. following:  we are given a specification K, which we call the retrieval key, and
  184. we must extract from the database all the programs that are correct with 
  185. respect to K.  In order to determine these, a graph traversal algorithm must be
  186. invoked to match K against the nodes Ri.  Specification K, as well as the nodes
  187. of the graph, are represented by logical formulas, which involve domain-specific
  188. predicates.
  189. Matching K against a node to determine which is greater (by the refinement 
  190. ordering) can be formulated as a first order logic theorem.  We are using 
  191. Otter's syntax to formulate such theorems, and are using Otter to prove (or 
  192. disprove) these theorems.  As an illustrative example, we have automated the 
  193. proofs involved in the retrieval operations of a database containing Pascal 
  194. compilers [NBM92] - clearly a non-trivial problem.  What we have found most 
  195. encouraging about the use of theorem prover, is that it requires little domain 
  196. knowledge about compiler construction before it can make inferences about 
  197. compilers and compiler specifications.
  198.  
  199. Our preliminary experience with the first prototype, and our experimentation 
  200. with the Otter theorem prover [LWB92] lead us to support the position that 
  201. formal methods can achieve a reasonable level of automation in software reuse, 
  202. thus affording us more precision and more efficiency.
  203.  
  204.  
  205. 3  Comparison 
  206.  
  207. The approaches to software description pursued by different research groups 
  208. vary widely.  These range from the simple unidimensional, key-based 
  209. classifications to multidimensional approaches rooted in modern library 
  210. sciences, such as the facetted approach [PDF87], to the rather non-standard 
  211. proposals such as linguistic approaches [PHZ91], or cognitive approaches [MS91].
  212.  
  213. In our previous work on the "Software Archive" we have built a stratified 
  214. multidimensional classification structure [MR87].  In this structure, components
  215. have been coarsely placed according to their degree of comprehensiveness, their
  216. functionality, and representational form, as well as according to their relative
  217. alikeness (IS-A hierarchy). The resulting structure was further refined by 
  218. (verbal) descriptive information. The implementation of this "Archive" [RM89] 
  219. could further support multiple user views, in order to allow different users to
  220. classify components according to their specific frame of reference.
  221.  
  222. The entries in the various classificatory dimensions have been - as with most 
  223. other approaches - strictly verbal. Depending on the specific classificatory 
  224. dimension, the administrator of the repository could either use keywords from a
  225. given list of descriptors or choose some descriptor formed according to locally
  226. defined rules (focus of the toolkit has been in-house reuse, where naming 
  227. conventions could be observed and a dictionary would suffice to supply all the 
  228. information needed for disambiguation).  With the completion of the 
  229. implementation of the Augusta prototype [Hoc92] of the "Software Base"-concept
  230. [MO87] the need for sharper discrimination among components becomes evident; we
  231. share this observation with other groups working on highly focussed libraries. 
  232.  
  233. Hence the need arises for more formal approaches.  Traditionally, formal 
  234. approaches to software reuse vary from algebraic specifications [MG91] to 
  235. specifications which have the form of high level programming languages [DS91].
  236.  
  237. The main differences between existing formal approaches and the approach we are
  238. taking lies in the fact that we strive for strict implementation independence. 
  239. This allows us to establish relationships among specifications, and hence among
  240. the programs bound to them, irrespective of any programming details and 
  241. implementation idiosyncracies. Since the specification components of database 
  242. entries may be arbitrarily abstract, hence may have arbitrarily simple 
  243. descriptions, an automatic inference mechanism can be entrusted with the duty 
  244. of checking properties of these entries (such as e.g. whether the specification
  245. component of an entry is is greater than a retrieve key).  Furthermore, it 
  246. allows the description of components on a relatively high level, where the 
  247. predicate part need not be fully descriptive; these predicates may (as long as 
  248. in-house reuse remains a target) build on tacit knowledge within the 
  249. application domain served by a particular component repository.
  250.  
  251.  
  252. References
  253.  
  254.  
  255. [DS91]  E.E. Doberkat and H.G. Sobottka.  A set oriented description language 
  256.     for ada.  In Proceedings, First International Workshop on Software 
  257.     Reusability, pages 193--197, 1991.
  258.  
  259. [Hoc92] E. Hochmueller.  Augusta: Eine reuse- orientierte software 
  260.     entwicklungsumgebung zur erstellung von ada-applicationen.  Technical 
  261.     report, Universitaet Klagenfurt, 1992.
  262.  
  263. [LWB92] E. Lusk L. Wos, R. Overbeek and J. Boyle.  Automated Reasoning: 
  264.     Introduction and Applications.  McGraw Hill, New York, NY, 1992.
  265.  
  266. [MG91]  Th. Moineau and M.C. Gaudel.  Software reusability through formal 
  267.     specifications.  In J. Cramer R. Prieto-Diaz, W. Schaefer and S. Wolf, 
  268.     editors, Proceedings, First International Workshop on Software 
  269.     Reusability, number Memo Nr 57 in UniDo, Dortmund, 1991.
  270.  
  271. [MO87]  R.T. Mittermeir and M. Oppitz.  Software bases for the flexible 
  272.         composition of application systems.  IEEE Trans. on Software 
  273.     Engineering, SE-13(4):440--460, April 1987.
  274.  
  275. [MR87]  R. Mittermeir and W. Rossak.  Software bases and software archives, 
  276.     alternatives to support software reuse.  In Proceedings, Fall Joint 
  277.     Computer Conference '87, pages 21--28, Dallas, October 1987.
  278.  
  279. [MS91]  N.A.M. Maiden and A.G. Sutcliffe.  Reuse of analogous specifications 
  280.     during requirements analysis.  In Proceedings, sixth International 
  281.     Workshop on Software Specification and Design, pages 220--223, Como, 
  282.     Italy, 1991.
  283.  
  284. [NBM92] A. Mili N. Boudriga and R.T. Mittermeir.  Semantic-based software 
  285.     retrieval to support rapid prototyping.  Structured Programming, 
  286.     13:109--127, 1992.
  287.  
  288. [PDF87] R. Prieto-Diaz and P. Freeman.  Classifying software for reusability.
  289.         IEEE Software, 4(1):6--16, 1987.
  290.  
  291. [PHZ91] C. Boldyreff P.A.V. Hall and J. Zhang.  Practitioner: Pragmatic support
  292.         for the reuse use of concepts in existing software.  In L. Dusink and 
  293.     P. Hall, editors,  Software Reuse, Utrecht 1989, pages 97--108. 
  294.     Springer-Verlag, 1991.
  295.  
  296. [RM89]  W. Rossak and R.T. Mittermeir.  A dbms based repository for reusable 
  297.     software components.  In Proceedings of the Second International 
  298.     Workshop Software Engineering and Its Applications, pages 501--518, 
  299.     Toulouse, France, 1989.
  300.  
  301.  
  302. Biography 
  303.  
  304. Ali Mili holds a PhD in computer science from the University of Illinois at 
  305. Urbana Champaign.  His research interests are software specifications, program 
  306. construction and software reuse.
  307.  
  308. Rym Mili holds a doctorate of specialty  from the University of Tunis, Tunisia.
  309. Her research interests are software specifications, compiler construction and 
  310. logic programming.
  311.  
  312. Roland Mittermeir is professor at the Institut fur Informatik at the 
  313. Universitat Klagenfurt, Austria.  Among his early work on software reuse is the
  314. design of the "Software Base"-Concept, now implemented in the AUGUSTA 
  315. environment. Recently, he has also worked on implementing reuse concepts in 
  316. medium sized software companies. Prof. Mittermeir holds degrees from the 
  317. Wirtschaftsuniversitat Wien and the Technische Universitat Wien.
  318.