Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!cs.utexas.edu!uunet!motcid!schultz
From: schultz@cell.mot.COM (Rob Schultz)
Newsgroups: comp.ai
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <783@carmine9.UUCP>
Date: 15 Jan 90 14:31:59 GMT
References: <25711@cup.portal.com> <1449@krafla.rhi.hi.is> <1990Jan11.015531.20996@world.std.com> <548@tci.bell-atl.com> <1990Jan12.030424.1397@world.std.com>
Organization: Motorola Inc. - Cellular Infrastructure Div., Arlington Heights, IL 60004
Lines: 27

bzs@world.std.com (Barry Shein) writes:

...deleted...

>The halting problem states (very roughly) "There exists at least one
>program who's halting conditions cannot be determined".

>People don't often write that program*, the fact that there was one
>(or a few) theoretically possible counter-example would hardly be
>sufficient to invalidate the concept of automatic program
>verification.

What about real-time/embedded software? If that type of software were to halt,
an error must have ocurred! In general, embedded software is written as an
infinite loop, with no way to exit (except to reset the processor). Does this
mean that even if we can verify "normal" software, we cannot verify embedded
software?

...deleted...

>-- 
>        -Barry Shein
-- 
Thanks -            Rob Schultz, Motorola General Systems Group
     rms          1501 W Shure Dr, Arlington Heights, IL  60004
708 / 632 - 2757   schultz@mot.cell.COM   !uunet!motcid!schultz
"There is no innocence - only pain."        (Usual disclaimers)