Return to BSD News archive
Path: euryale.cc.adfa.oz.au!newshost.anu.edu.au!harbinger.cc.monash.edu.au!news.bhp.com.au!mel.dit.csiro.au!munnari.OZ.AU!spool.mu.edu!howland.reston.ans.net!gatech!swrinde!sgigate.sgi.com!wetware!spunky.RedBrick.COM!nntp.et.byu.edu!news.byu.edu!hamblin.math.byu.edu!park.uvsc.edu!usenet
From: Terry Lambert <terry@lambert.org>
Newsgroups: comp.unix.bsd.freebsd.misc,comp.os.linux.development.system
Subject: Re: The better (more suitable)Unix?? FreeBSD or Linux
Date: 23 Feb 1996 22:40:07 GMT
Organization: Utah Valley State College, Orem, Utah
Lines: 44
Message-ID: <4glfo7$8b@park.uvsc.edu>
References: <4er9hp$5ng@orb.direct.ca> <4f9skh$2og@dyson.iquest.net> <ALBERT.96Feb22220117@krakatoa.ccs.neu.edu>
NNTP-Posting-Host: hecate.artisoft.com
Xref: euryale.cc.adfa.oz.au comp.unix.bsd.freebsd.misc:14354 comp.os.linux.development.system:18006
albert@krakatoa.ccs.neu.edu (Albert Cahalan) wrote:
] Proofs are great for filesystem development.
] They are useless for testing; you should know this.
]
] You can "prove" that something works, but how can you be sure
] that the code matches your proof?
By performing a full branch path analysis to generate test
cases the fully exercise the code, and then making sure the
test results conform to the spec.
CASE tools, like "Battlemap Anaysis" can automate much (or all)
of this process.
] Yeah, you read it. So what. People make bad proofreaders
] because they see what they expect to see. You can prove that
] a fictional filesystem works, but you can only test, test,
] and retest a real filesystem. We're not talking about
] hello_world.c here. Even if the code really is good (only
] God knows for sure), you can hit compiler bugs.
Compiler bugs would show in regression testing using the BPA
test clauses.
] Maybe you will make a mistake in your reasoning.
That's always possible. 8-).
] You can _never_ prove that your filesystem is correct,
] but you can test it.
You can prove that it matches the specification, and you can
modify the specification if you made a mistake in your reasoning.
Proving compliance with a spec is what validation suites are all
about.
Terry Lambert
terry@cs.weber.edu
---
Any opinions in this posting are my own and not those of my present
or previous employers.