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

[M.Y.W.Y. Becker]

--On 04 June 2001 20:53 +0100 Raymond Chan <rwlc3@cam.ac.uk> wrote:

>> 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?

Using VCs should be ok unless it says explicitly you must use some other 
form of proof.

Mo