Abstract
Static code analysis originally concerned the extraction from source code of various properties of a program. Although this kind of reverse engineering approach can uncover errors that are hard to detect in other ways, it is not a very efficient use of resources because of its retrospective nature and the late error detection that results. The SPARK language and its associated Examiner tool took a different approach which emphasises error prevention (“correctness by construction”) rather than error detection. Recent work with SPARK has shown that very early application of static analysis can have a beneficial influence on software architectures and designs. The paper describes the use of SPARK to produce designs with demonstrably low coupling and high cohesion.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Croxford, Martin and Sutton, James. Breaking through the V&V Bottleneck. Lecture Notes in Computer Science Volume 1031, 1996.
Sutton, James. Cost-Effective Approaches to Satisfy Safety-critical Regulatory Requirements. Workshop Session, SIGAda 2000.
B.D. Bramson. Malvern’s Program Analysers. RSRE Research Review 1984.
Bernard Carré. Program Analysis and Verification in High Integrity Software. Chris Sennett (Ed). Pitman. ISBN 0-273-03158-9.
C. Daniel Cooper. Ada Code Analysis: Technology, Experience, and Issues. Proceedings SIGAda 2000.
Finnie, Gavin et al. SPARK-The SPADE Ada Kernel. Edition 3.3, 1997, Praxis Critical Systems.
Finnie, Gavin et al. SPARK 95-The SPADE Ada 95 Kernel. 1999, Praxis Critical Systems.
Barnes, John. High Integrity Ada-the SPARK Approach. Addison Wesley Longman, ISBN 0-201-17517-7.
King, Hammond, Chapman and Pryor. Is Proof More Cost-Effective than Testing?. IEEE Transaction on Software Engineering, Vol. 26, No. 8, August 2000, pp. 675–686.
Bergeretti and Carré. Information-flow and data-flow analysis of while-programs. ACM Transactions on Programming Languages and Systems, 1985, pp. 37–61.
Amey, Peter. The INFORMED Design Method for SPARK. Praxis Critical Systems 1999, 2001.
D.L. Parnas and J. Madey. Functional Documentation for Computer Systems, in Science of Computer Programming. October 1995. pp. 41–61.
Amey, Peter. A Language for Systems not Just Software. Proceedings, SIGAda 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Amey, P. (2002). Closing the Loop: The Influence of Code Analysis on Design. In: Blieberger, J., Strohmeier, A. (eds) Reliable Software Technologies — Ada-Europe 2002. Ada-Europe 2002. Lecture Notes in Computer Science, vol 2361. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48046-3_12
Download citation
DOI: https://doi.org/10.1007/3-540-48046-3_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43784-0
Online ISBN: 978-3-540-48046-4
eBook Packages: Springer Book Archive