Question about run-time checks

Nov 15, 2011 at 8:21 PM

Hi,

When the static verification in Spec# is enough and when the compiler will emits run-time checks for contracts already passed the static verification?

I still did not get an answer for my previous question about a compiler internal error, although I posted the code.

Thanks,

Adnan

Developer
Nov 17, 2011 at 7:35 AM

Hi,

are you asking if the runtime checks are only emitted for assertions that didn't pass the verification? If so, the answer is no. However, the idea of removing some of the runtime checks, if the corresponding assertions were verified, seems interesting.

Best regards,

Valentin

Nov 17, 2011 at 3:38 PM

Hi,

The Spec# tutorial document saying that static verification proves that the implementation will not violate the assertions. Although I understand that there will be some assertions will still need run-time check for obvious reasons but I thought that for example assertions that already have all their data inside the implementation will not produce run-time checks; Or assertions that has been proved by deduction that there is no way to violate them if  some preconditions hold. 

Now my question is: If a peice of a code is verified under the assumption that some conditions and constraints hold when this peice of code started, in this case provided that it is guaranteed that those conditions and constraints hold, can I rely only on the static verification of spec# and avoid the run-time checks ?

Thanks,

Adnan

Developer
Nov 18, 2011 at 10:29 AM

Hi Adnan,

generally static verification can't fully replace testing or runtime checking. Static verification for general-purpose programming languages usually does not check for every possible error (e.g., stack overflow, arithmetic overflows). Therefore you cannot rely on static verification exclusively. However, it might be desirable to remove certain runtime checks if you can guarantee that they can never be violated. Currently Spec# doesn't do this.

Best regards,

Valentin