Question

Prepare a computer program that accepts, as input, programs in some programming language together with optional assertions, and that attempts to fill in the remaining assertions necessary to make a proof that the computer program is valid. For example, strive to get a program that is able to prove the validity of Euclid's Algorithm, given only assertions 1,4,and 6. See the papers by R. W. Floyd and J.C. King in the IFIP Congress proceedings for further discussion


HELP!!!!!!

Answer 1

so basically, write a computer programs that proves other programs :-P

Answer 2

your question are getting hard

Answer 3

? my brain hurts

Answer 4

I'll use python for everything :-P. I'll code up euclid's algorithm (it's only like 4 lines in python). How do I do the proof part? I think it's by induction

Answer 5

I can imagine the question writer grinning and gloating... "So now you know how to do proofs by induction. But the real question is... can you program it? :-D"

Answer 6

aaaaaaaaaaaaaaaahhhhhhhhhhh

Answer 7

http://dl.acm.org/citation.cfm?id=808444

Answer 8

http://dl.acm.org/citation.cfm?id=805820&dl=ACM&coll=DL&CFID=70418575&CFTOKEN=46157586