allen@gitpyr.UUCP (P. Allen Jensen) (08/18/85)
It seems to me that using Logic as both a specification language and a
programming language would make the problem of Verification and
program Synthesis eaiser. Deduction may be used to both derive
programs from their specification and to run those programs. On the
other hand, wouldn't using Logic for both tend to make the difference
between the specification and the program fuzzy ?
I understand how a specification can be used to verify a program. This
assumes, however, that the specification is correct and self-consistent.
It would seem that this is just as difficult as writing a correct
program ! How does one verify a specification ?
P. Allen Jensen
--
P. Allen Jensen
Department of Civil Engineering
Georgia Insitute of Technology, Atlanta Georgia, 30332
...!{akgua,allegra,amd,hplabs,ihnp4,masscomp,ut-ngp}!gatech!gitpyr!allenshebs@bcsaic.UUCP (stan shebs) (08/21/85)
In article <663@gitpyr.UUCP> allen@gitpyr.UUCP (P. Allen Jensen) writes: >I understand how a specification can be used to verify a program. This >assumes, however, that the specification is correct and self-consistent. >It would seem that this is just as difficult as writing a correct >program ! How does one verify a specification ? Difficulty of specification depends on what you want to specify. Out in the real world, a specification might read something like "this program will cause the cruise missile to reach its target and kill millions of Russian babies", and of course verification is preferable to validation :-) Most specification end up being a little more detailed, however. Expert systems (and *some* logic programs) are in the position of having a specification as long as or longer than the program, so it's preferable to make the specification *be* the program... stan shebs bcsaic!shebs
nabiel@erix.UUCP (Nabiel Elshiewy) (08/21/85)
In article <663@gitpyr.UUCP> allen@gitpyr.UUCP (P. Allen Jensen) writes: > >I understand how a specification can be used to verify a program. This >assumes, however, that the specification is correct and self-consistent. >It would seem that this is just as difficult as writing a correct >program ! How does one verify a specification ? > >P. Allen Jensen Well, specify it and use the specification to verify the specification.