代码合同表明了一个同义前提条件 [英] Code contracts suggests a tautological precondition

问题描述

 
< Extension（）> <纯（）> 
 公共 功能 FloorMultiple（ ByVal 值作为 UInt16， ByVal  divisor 作为 UInt16）作为 UInt16 
 Contract.Requires（除数> 0）
 Contract.Ensures（Contract.Result（ OF UInt16）（） Mod  divisor = 0）
 Contract.Ensures（Contract.Result（Of UInt16）（）< = value）
 Contract.Ensures（Contract.Result（Of UInt16）（）+ divisor> value）
 返回值 - 值 Mod 除数
 结束 功能 
 
 

解决方案

您好Strilanc，

 谢谢你的举报。现在它已修复（实际上第三个后置条件已被证实）

 

谢谢，

f

    <Extension()> <Pure()>
    Public Function FloorMultiple(ByVal value As UInt16, ByVal divisor As UInt16) As UInt16
      Contract.Requires(divisor > 0)
      Contract.Ensures(Contract.Result(Of UInt16)() Mod divisor = 0)
      Contract.Ensures(Contract.Result(Of UInt16)() <= value)
      Contract.Ensures(Contract.Result(Of UInt16)() + divisor > value)
      Return value - value Mod divisor
    End Function

解决方案

Hi Strilanc,

  thank you for reporting it. Now it is fixed (actually the third postcondition is proven)

 

Thanks,

f

这篇关于代码合同表明了一个同义前提条件的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！