[CST-2] Spec & Ver I (Style of proof)

Raymond Chan rwlc3@cam.ac.uk
Mon, 4 Jun 2001 20:53:56 +0100


> is it ok to use either VC or doing
> it using the H-Logic inference rules, etc?  Or is there any catch phase
that
> one should watch out for?

I personally prefer using VCs - BUT - what do people think about the way
questions are worded, e.g. 99p7q2: "Give a detailed proof using Floyd-Hoare
logic that... " - does that exclude the use of VCs? His model answer online
is a proof with inference rules, do you think using VCs in that question
isn't quite what is being asked for?

Raymond