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 / wisr6 / proceedings / ascii / mittermeir2.ascii < prev    next >
Text File  |  1993-10-19  |  16KB  |  393 lines
  1.  
  2.  
  3.  
  4.  
  5.  Building  A  Repository  of  Software Components:  A  Formal
  6.  
  7.  
  8.                                   Specifications Approach
  9.  
  10.  
  11.  
  12.                                              R.T. Mittermeir
  13.  
  14.  
  15.  
  16.                                         Institut fur Informatik
  17.  
  18.                                         Universit{t Klagenfurt
  19.  
  20.                                      A-9022 Klagenfurt, Austria
  21.  
  22.                               e-mail: roland@samos.ifi.uni-klu.ac.at
  23.  
  24.  
  25.  
  26.                                              R. Mili, A. Mili
  27.  
  28.  
  29.  
  30.                                           University of Ottawa
  31.  
  32.                                  Department of Computer Science
  33.  
  34.                                   Ottawa, Ont. K1N 6N5 Canada
  35.  
  36.                                e-mail: frmili,amilig@csi.uottawa.ca
  37.  
  38.  
  39.  
  40.                                                   Abstract
  41.  
  42.  
  43.     In our correspondence to the fifth Workshop on Software Reuse [1], we had discussed the
  44. design and preliminary implementation of a repository where software components can be stored
  45. and retrieved automatically, using a formal-specification approach. In this paper we report on
  46. our progress, by describing the first prototypes we have for this repository, as well as preliminary
  47. assessment of their performance.
  48.  
  49.  
  50. Keywords:  formal specification, program correctness, program refinement, theorem proving,
  51. software repositories, storage and retrieval of softwarecomp onents.
  52.  
  53.  
  54. Workshop Goals: assessing how our work fits in the overall problem of software reuse; iden-
  55. tifying potential partners for developing our system on a larger scale, and with sharper focus.
  56.  
  57.  
  58. Working Groups: reuse and formal methods, tools and environments, reuse process models,
  59. domain analysis and engineering, reuse handbook.
  60.  
  61.  
  62.  
  63.                                                Mittermeir- 1
  64.  
  65.  
  66. 1      Background
  67.  
  68.  
  69.  
  70. The approach advocated in this paper results from the combination of two research efforts:
  71.  
  72.  
  73.  
  74.     fflAn  effort  by  the  first  author  to  build  a  software  archive  as  a  stratified  multidimensional
  75.        classification structure for software components.
  76.  
  77.  
  78.     fflAn effort by the second and third authors to investigate various features of the specification
  79.        process and the specification product, as well as the construction and verification of programs.
  80.  
  81.  
  82.  
  83. In  a  recent  joint  publication  [2]  the  first  and  third  authors  make  a  proposal  for  constructing  a
  84. database of software components, based on the following premises:
  85.  
  86.  
  87.  
  88.     fflEntries of the database have the form of hspecification; programi pairs, where the program
  89.        component is correct with respect to the specification component.
  90.  
  91.  
  92.     fflThe set of database entries is structured by means of the refinement ordering between the
  93.        specification components of the entries.
  94.  
  95.  
  96.     fflThe retrieve key for retrieval operations on the database take the formof a sp ecification, and
  97.        seeks to determine all the programs of the database that are correct with respect to the key,
  98.        by matching the key against the specification components of database entries.
  99.  
  100.  
  101.  
  102. Our design rationale is that by representing database entries with arbitrarily abstract specifications
  103. and by letting the match between a store key and a retrieve key be defined by the refinement ordering
  104. (rather than strict equality), we deal effectively with the diversity of software components and the
  105. complexity of organizing such components in a database.
  106.  
  107.  
  108. In this position paper we report on our progress in implementing this software repository, using
  109. C  under  Unix, and  an  experimental  theorem  prover  (Otter, fclArgonne  National  Laboratory).
  110. Among the Functions we have implemented we mention: Storage of software components;Retrieval
  111. of software components;and Approximate Retrieval of software comp onents, to be invoked whenever
  112. (exact) retrieval fails to produce results.
  113.  
  114.  
  115.  
  116. 2      Position
  117.  
  118.  
  119.  
  120. 2.1     Statement of the Position
  121.  
  122.  
  123.  
  124. We  submit  the  position  that  the  storage  and retrieval  of  software components  in  an  automated
  125. software repository is technologically possible, provided these components are described by formal
  126. specifications. This means in principle that software designers can use off-the-shelf software, in the
  127. same manner as hardware designers make use of off-the-shelf hardware to design hardware systems.
  128.  
  129.  
  130. We qualify this position slightly, by adding that although the storage and retrieval is possible, it
  131. is not (yet) efficient: the theorem proving parts of our system remain something of a bottleneck
  132. (proofs can take unreasonably long).
  133.  
  134.  
  135. To place our position in context, we add two premises:
  136.  
  137.  
  138.                                                       Mittermeir- 2
  139.  
  140.  
  141.     fflFirst, we realize that there is a great deal more to software reuse than the mere mechanics
  142.        of storing and retrieving software components; more important than storing and retrieving
  143.        components is the ability to design components that are worthy of reuse;also more important
  144.        is the ability to define design methodologies that make use of reusable components. On the
  145.        other hand, as several authors point out [3 , 4, 5 , 6 ], software reuse is as much (if not more)
  146.        a managerial and organizational challenge as it is a technological challenge.
  147.  
  148.  
  149.     fflSecond,  our pattern of software reuse depends on programs being specified formally.  In an
  150.        organization that does not practice formal methods, it may or may not be cost effective to
  151.        formally specify software components for the sole purpose of integrating them in a software
  152.        repository. On the other hand, one might argue that the use of formal methods is cost-effective
  153.        on its own merits [7 ].
  154.  
  155.  
  156.  
  157. To motivate our position (and illustrate the extent of its validity) we give below some detailsab out
  158. the implementation of our system.
  159.  
  160.  
  161.  
  162. 2.2     Substantiating the Position
  163.  
  164.  
  165.  
  166. In this section we give very summary details ab out the implementation of our system.  First, we
  167. discuss its overall architecture.
  168.  
  169.  
  170. In any database system, the key to efficient retrieval is the availability of an ordering between the
  171. database entries. Typically, database entries are totally ordered, i.e. for any two distinct entries,
  172. one is necessarily smaller than the other (for the given ordering).  For software components, we
  173. could not identify such a total ordering relation;hence, as a substitute, we defined a partial ordering
  174. relation, namely the refinement ordering. This gives our repository a lattice-like structure, where
  175. nodes represent specifications; and programs are attached to specifications in such a way that each
  176. program is attached to the highest specification with respect to which it is correct.  This integrity
  177. constraint must be maintained by all database op erations.  As an example of a database structure,
  178. see in figure 1 the database obtained by storing a number of Pascal compilers, whose definition is
  179. given in [2].  Each node in this graph represents asp ecification;  to each node we attach programs
  180. that are correct with respect to the specification that this node represents (these are not shown in
  181. the figure).
  182.  
  183.  
  184. Storage  and  retrieval  operations  consist  of  navigating  through  a  graph  structure,  matching  the
  185. (storage or retrieval) key against nodes of the graph.  Each node of the graph is represented by
  186. a  Unix  file  which  contains  an  Otter  formula  that  defines  the  specification  at  hand,  as  well  as
  187. information on neighboring nodes in the graph, and information on programs that are attached to
  188. this node.
  189.  
  190.  
  191. The navigation through the graph is carried out bytraditional graph traversal algorithms _which
  192. we have implemented in C under Unix. The matching of the (storage or retrieval) key against the
  193. current node is carried out in two steps: first we generate an Otter theorem that states that the
  194. key is a refinement of the current node; then we submit this theorem to the Otter theorem prover
  195. and await its result. The theorem prover and our C program interact to determine the result and
  196. act accordingly.
  197.  
  198.  
  199. Whenever exact retrieval fails, the user has the option of invoking approximate retrieval. Approx-
  200. imate  retrieval  is  defined  in  terms  of  a  measure  of  functional  proximity  between  specifications,
  201. which measures how close twosp ecifications are by assessing how much information they have in
  202.  
  203.  
  204.  
  205.                                                       Mittermeir- 3
  206.  
  207.  
  208.  
  209.  
  210.  
  211.  
  212.                                                                                               _
  213.  
  214.  
  215.  
  216.  
  217.                                                 @ @
  218.                                                _                              _
  219.                                                 @   @  @
  220.                                                   @
  221.                                                      @    @ @
  222.                                                         @
  223.                                 @ @                       @
  224.                                 _    @                      @  _
  225.                                 @      @
  226.                                   @       @
  227.                                      @       @
  228.                                        @
  229.                                           @
  230.                                              @ _
  231.  
  232.  
  233.  
  234.                                    Figure 1: A Repository of Pascal Compilers
  235.  
  236.  
  237.  
  238. common.  We have determined that a lattice operator,  namely the meet (greatestlower bound)
  239. captures precisely the amount of information that two specifications have in common.  The algo-
  240. rithm of approximate retrieval for a given retrieval key k proceeds by computing the meet of k
  241. with nodes in the graph, and identifying those noodes that maximize the meet with k (i.e.  that
  242. have most common information with k).  In the compiler example,  the graph that we obtain by
  243. computing the meet of all nodes with k, for some retrievalk which is given in [2 ],is shown in figure
  244. 2.  Note that this is obtained from the original graph by collapsing its two layers: whenever two
  245. nodes are collapsed, we can conclude that they differ by functional properties that are irrelevant
  246. as far as k is concerned; i.e. as far as k is concerned, one node is as good as another.  In practice,
  247. this algorithm has given results that are quite satisfactoryto the intuition.
  248.  
  249.  
  250.  
  251. 3      Comparison
  252.  
  253.  
  254.  
  255. Our  work  deals  with  the  problem  of  storing  and  retrieving  software  components  using  a  formal
  256. specification  approach.  As  such, it  must  be  compared  with  alternative  methods  of  storage  and
  257. retrieval of software components as well as alternative methods of software reuse based on formal
  258. specifications.
  259.  
  260.  
  261. Alternative methods of storage and retrieval of software components include the facetted approach,
  262. due to Prieto-Diaz and Freeman [8], the linguistic approach, due to Hall et al [9], and the cogni-
  263. tive approach, due to Maiden and Sutcliffe [10 ]. All these approaches are inspired from retrieval
  264. techniques of library science, and carry the usual drawbacks of natural language methods.
  265.  
  266.  
  267. Alternative methods of using formal specifications for the purpose of software reuse include work
  268.  
  269.  
  270.  
  271.                                                       Mittermeir- 4
  272.  
  273.  
  274.  
  275.  
  276.  
  277.                                                                                               o
  278.  
  279.  
  280.  
  281.  
  282.                                                 o                              o
  283.                                                 @
  284.                                                   @
  285.                                                      @
  286.                                                         @
  287.                                                           @
  288.                                 o                           @  o
  289.                                 @
  290.                                   @
  291.                                      @
  292.                                        @
  293.                                           @
  294.                                              @  o
  295.  
  296.  
  297.  
  298.                                Figure 2:  Ordering Nodes by their Proximity to k.
  299.  
  300.  
  301.  
  302. by Moineau and Gaudel [11 ] as well as work by Srinivas and Goldberg [12 ].  We differ from both
  303. of these proposals by the formal specifications background that we use:  ours is relational, dealing
  304. primarily with functional descriptions of softwarecomp onents,  whereas thealternative proposals
  305. use  algerbraic  specifications, dealing  with  descriptions  of  software components  as  state  bearing
  306. modules. Furthermore we differ from the work of Srinivas by the fact that we concentrate on reusing
  307. software products, whereas they focus on reusing software processes (e.g.  previously recorded design
  308. scenarii).
  309.  
  310.  
  311.  
  312. References
  313.  
  314.  
  315.  
  316.   [1] R. M. A. Mili and R. Mittermeir, "A formal approach to software reuse: Design and imple-
  317.       mentation," in Proceedings, Fifth Workshop on Software Reuse, 1992.
  318.  
  319.  
  320.   [2] A. M. N. Boudriga and R. Mittermeir, "Semantic-based software retrieval to support rapid
  321.       prototyping," Structured Programming, vol. 13, pp. 109-127, 1992.
  322.  
  323.  
  324.   [3] P.  Collins,  "Considering  corporate  culture  in  institutionalizing  reuse,"  in  Proceedings,  Fifth
  325.       Workshop on Software Reuse, 1992.
  326.  
  327.  
  328.   [4] S. Fraser, "Reuse by design- a team approach,"  in Proceedings, Fifth Workshop on Software
  329.       Reuse, 1992.
  330.  
  331.  
  332.   [5] M. Griss, "A multi-disciplinary software reuse research program," in Proceedings, Fifth Work-
  333.       shop on Software Reuse, 1992.
  334.  
  335.  
  336.   [6] K.  Wentzel, "Software  reuse-  it's  a  business," in  Proceedings,  Fifth  Workshop  on  Software
  337.       Reuse, 1992.
  338.  
  339.  
  340.                                                       Mittermeir- 5
  341.  
  342.  
  343.   [7] J. Guttag and J. Horning, Larch: Languages and Tools for Formal Specification. New York,
  344.       NY: Springer Verlag, 1993.
  345.  
  346.  
  347.   [8] R. Prieto-Diaz and P. Freeman, "Classifying software for reusability," IEEE Software, vol. 4,
  348.       no. 1, pp. 6-16, 1987.
  349.  
  350.  
  351.   [9] C. B. P.A.V. Hall and J. Zhang,"Practitioner: Pragmatic support for the reuse use of concepts
  352.       in existing software,"in Software Reuse, Utrecht 1989 (L. Dusink and P. Hall, eds.), pp.97-108,
  353.       Springer-Verlag, 1991.
  354.  
  355.  
  356. [10]  N. Maiden and A. Sutcliffe, "Reuse of analogous specifications during requirements analysis,"
  357.       in Proceedings,  sixth  International  Workshop  on  Software  Specification  and  Design, (Como,
  358.       Italy), pp. 220-223, 1991.
  359.  
  360.  
  361. [11]  T. Moineau and M. Gaudel, "Software reusability through formal specifications," in Proceed-
  362.       ings, First International Workshop on Software Reusability (J. C. R. Prieto-Diaz, W. Schaefer
  363.       and S. Wolf, eds.), no. Memo Nr 57 in UniDo,(Dortmund), 1991.
  364.  
  365.  
  366. [12]  Y. Srinivas and A. Goldberg, "Replay of derivation histories in kids," in Proceedings, Fifth
  367.       Workshop on Software Reuse, 1992.
  368.  
  369.  
  370.  
  371. 4      Biography
  372.  
  373.  
  374.  
  375. Roland Mittermeir is professor at the Institut fur Informatik at the Universit{t Klagenfurt, Aus-
  376. tria.  Among his early work on software reuse is the design of the "Software Base"-Concept, now
  377. implemented in the AUGUSTA environment. Recently, he has also worked on implementingreuse
  378. concepts in medium sized software companies.  Prof.  Mittermeir holds degrees from the Wirtschaft-
  379. suniversit{t Wien and the Technische Universit{t Wien.
  380.  
  381.  
  382. Rym  Mili  holds  a  doctorate of  specialty  from  the  University  of  Tunis,  Tunisia,  and  is  currently
  383. working towards a PhD at the University of Ottawa under the supervision of Professor Robert L.
  384. Probert. Her research interests are software specifications, softwaretesting, and software reuse.
  385.  
  386.  
  387. Ali Mili holds a PhD in computer science from the University of Illinois atUrbana Champaign.
  388. His research interests are software specifications, program construction and software reuse.
  389.  
  390.  
  391.  
  392.                                                       Mittermeir- 6
  393.