The logic of software design
The logic of software design
- Author(s): J.S. Ostroff and R.F. Paige
- DOI: 10.1049/ip-sen:20000681
For access to this article, please select a purchase option:
Buy article PDF
Buy Knowledge Pack
IET members benefit from discounts to all IET publications and free access to E&T Magazine. If you are an IET member, log in to your account and the discounts will automatically be applied.
Thank you
Your recommendation has been sent to your librarian.
- Author(s): J.S. Ostroff 1 and R.F. Paige 1
-
-
View affiliations
-
Affiliations:
1: Department Of Computer Science, York University, Toronto, Canada
-
Affiliations:
1: Department Of Computer Science, York University, Toronto, Canada
- Source:
Volume 147, Issue 3,
June 2000,
p.
73 – 80
DOI: 10.1049/ip-sen:20000681 , Print ISSN 1462-5970, Online ISSN 1463-9831
The authors provide an overview of how logic can be used throughout the software development cycle, and discuss what methods can be introduced in the computer science curriculum to support software development. To see how logic is useful throughout the cycle, they present the WRSM reference model, and illustrate it with simple motivating examples. Reasoning is performed in Logic E, and PVS is used to illustrate automated proofs.
Inspec keywords: formal logic; computer science education; software engineering
Other keywords:
Subjects: Software engineering techniques; Computing education and training; Formal logic
References
-
-
1)
- J.-R. ABRIAL . (1996) , The B-Book: Assigning programs to meanings.
-
2)
- J.E. PAYNE , M.A. SCHATZ , M.N. SCHMID . Implementing assertions for Java. Dr. Dobb's Journal , 40 - 44
-
3)
- S. OWRE , J. RUSHBY , N. SHANKAR , F.V. HENKE . Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Trans. Softw. Eng. , 2 , 107 - 125
-
4)
- J.R. BURCH , E.M. CLARKE , K.L. MACMILLAN , D.L. DILL , L.J. HWANG . Symbolic model checking: 10∧20 states and beyond. Inf. Comput. , 2 , 142 - 170
-
5)
- PAIGE, R.F. and OSTROFF, J.S. `An object-oriented refinement calculus'. Department. of Computer Science, York University, Toronto. CS-1999-07, 1999. http://www.cs.yorku.ca/techreports/1999/CS-1999-07.html.
-
6)
- D. GRIES , F.B. SCHNEIDER . (1993) , A logical approach to discrete math.
-
7)
- T.S. PERRY . Donald O. Pederson. IEEE Spectr. , 6 , 22 - 27
-
8)
- OSTROFF, J.S. and R.F. PAIGE. `The timed predicative calculus as a framework for comparative semantics'. York University. CS-2000-01, 2000. http://www.cs.yorku.ca/techreports/2000/CS-2000-01.html.
-
9)
- B. Meyer . (1988) , Object-oriented software construction.
-
10)
- R.L. GLASS . The software research crisis. IEEE Softw. , 6 , 42 - 47
-
11)
- NASA. Formal methods specification and analysis guidebook. NASA Office of Safety and Mission Assurance. NASA-GB-001-97, 1997..
-
12)
- M. HUTH , M. RYAN . (1999) , Logic in computer science: Modelling and reasoning about systems.
-
13)
- D.L. PARNAS , P.C. CLEMENTS . A rational design process: How and why to fake it. IEEE Trans Softw. Eng. , 2 , 251 - 257
-
14)
- G. HOLZMANN . The model checker spin. IEEE Trans Softw. Eng. , 5 , 279 - 295
-
15)
- GRIES D., On presenting monotoncity and on EA => AE. Cornell University, Department of Computer Science, TR95-1512, 1995, http://www.cs.cornell.edu/gries/Papers/Monotonicity.ps.
-
16)
- D.L. PARNAS , J. MADEY . Functional documentation for computer systems. Sci. Comput. Program. , 41 - 61
-
17)
- OSTROFF, J.S. and R. PAIGE. `The logic of software design'. Computer Science, York University. CS-98-04, 1998. http://www.cs.yorku.ca/General/techreports/98/CS-98-04.html.
-
18)
- E.C.R. HEHNER . (1993) , A practical theory of programming.
-
19)
- C.N. DEAN , M.G. HINCHEY . (1996) , Teaching and learning formal methods.
-
20)
- C. Morgan . (1994) , Programming from specifications.
-
21)
- A. HALL . Seven myths of formal methods. IEEE Softw. , 5 , 11 - 19
-
22)
- D.L. PARNAS , J. MADEY , M. IGLEWSKI . Precise documentation of well-structured programs. IEEE Trans. Softw. Eng. , 12 , 948 - 976
-
23)
- C.A. GUNTER , E.L. GUNTER , M. JACKSON , P. ZAVE . A reference model for requirements and specifications. IEEE Softw. , 3 , 37 - 43
-
24)
- K. WALDEN , J.-M. NERSON . (1995) , Seamles object oriented software and architecture.
-
25)
- D. Gries . (1981) , The science of programming.
-
26)
- MANNA Z. `STeP'. The Stanford Temporal Prover. Dep. of Computer Science, Stanford University, STAN-CS-'TR-94-1518 1994.
-
27)
- BICARREGUI, J.C., DICK, A.J.J., WOODS, E.: `Quantitative analysis of an application of formal methods', In Proc. of FME'96, Third International Symposium of Formal Methods Europe, 1996, Springer-Verlag, LNCS 1051.
-
28)
- J.S. OSTROFF , J. KRAMER . (1989) , Temporal logic for real-time systems. Advanced software development series.
-
29)
- M. JACKSON . (1995) , Software requirements & specifications.
-
30)
- J.-M. JEZEQUEL , B. MEYER . Design by contract: the lessons of the ariane. IEEE Comput. , 1 , 129 - 130
-
31)
- M. HINCHEY , J. BOWEN . (1995) , Applications of formal methods.
-
1)
Related content
