liu.seSearch for publications in DiVA
Change search
ReferencesLink to record
Permanent link

Direct link
Semantic Inspection of Software Artifacts From Theory to Practice
Linköping University, Department of Computer and Information Science. Linköping University, The Institute of Technology.
2001 (English)Doctoral thesis, monograph (Other academic)
Abstract [en]

Providing means for the development of correct software still remains a central challenge of computer science. In this thesis we present a novel approach to tool-based inspection focusing on the functional correctness of software artifacts. The approach is based on conventional inspection in the style of Fagan, but extended with elements of formal verification in the style of Hoare. In Hoare’s approach a program is annotated with assertions. Assertions express conditions on program variables and are used to specify the intended behavior of the program. Hoare introduced a logic for formally proving the correctness of a program with respect to the assertions.

Our main contribution concerns the predicates used to express

assertions. In contrast to Hoare, we allow an incomplete axiomatization of those predicates beyond the point where a formal proof of the correctness of the program may no longer be possible. In our approach predicates may be defined in a completely informal manner (e.g. using natural language). Our hypothesis is, that relaxing the requirements on formal rigor makes it easier for the average developer to express and reason about software artifacts while still allowing the automatic generation of relevant, focused questions that help in finding defects. The questions are addressed in the inspection, thus filling the somewhat loosely defined steps of conventional inspection with a very concrete content. As a side-effect our approach facilitates a novel systematic, asynchronous inspection process based on collecting and assessing the answers to the questions.

We have adapted the method to the inspection of code as well as the inspection of early designs. More precisely, we developed prototype tools for the inspection of programs written in a subset of Java and early designs expressed in a subset of UML. We claim that the method can be adapted to other notations and (intermediate) steps of the software process. Technically, our approach is working and has successfully been applied to small but non-trivial code (up to 1000 lines) and designs (up to five objects and ten messages). An in-depth industrial evaluation requires an investment of substantial resources over many years and has not been conducted. Despite this lack of extensive assessment, our experience shows that our approach indeed makes it easier to express and reason about assertions at a high level of abstraction.

Place, publisher, year, edition, pages
Linköping: Linköping University Electronic Press, 2001. , 197 p.
Linköping Studies in Science and Technology. Dissertations, ISSN 0345-7524 ; 725
Keyword [en]
Software development process, programming, program language, UML
National Category
Computer Science
URN: urn:nbn:se:liu:diva-4975ISBN: 91-7373-208-7OAI: diva2:20841
Public defence
2001-12-14, Visionen, Hus B, Campus Valla, Linköpings universitet, Linköping, 10:15 (English)
Available from: 2002-01-16 Created: 2002-01-16 Last updated: 2012-01-24Bibliographically approved

Open Access in DiVA

fulltext(695 kB)560 downloads
File information
File name FULLTEXT01.pdfFile size 695 kBChecksum MD5
Type fulltextMimetype application/pdf

By organisation
Department of Computer and Information ScienceThe Institute of Technology
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 560 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 275 hits
ReferencesLink to record
Permanent link

Direct link