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

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
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.
Series
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
Identifiers
URN: urn:nbn:se:liu:diva-4975ISBN: 91-7373-208-7 (print)OAI: oai:DiVA.org:liu-4975DiVA: diva2:20841
Public defence
2001-12-14, Visionen, Hus B, Campus Valla, Linköpings universitet, Linköping, 10:15 (English)
Supervisors
Available from: 2002-01-16 Created: 2002-01-16 Last updated: 2012-01-24Bibliographically approved

Open Access in DiVA

fulltext(695 kB)596 downloads
File information
File name FULLTEXT01.pdfFile size 695 kBChecksum SHA-1
001b66b95bc98ba61fe074ea63bd739d729835f838d7fcaafe18d6a4c319a49e10ec3bce
Type fulltextMimetype application/pdf

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

Search outside of DiVA

GoogleGoogle Scholar
Total: 596 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

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 297 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf