PROSAGA码农传奇-Ada-后置条件的含义

0# 特狼普 | 2019-08-31 10-32

1# 丫头 | 2019-08-31 10-32

<div class =“post-text”itemprop =“text”>
  <P>
    对于后置条件，您必须根据子程序应对旧状态产生的影响来定义新状态。
  </p>
  <P>
    当后置条件说
     <code>
      post Pointer = Pointer~ +1
    </code>
    ，这意味着新的价值
     <code>
      Pointer
    </code>
     应该是旧值+ 1;即
     <code>
      Variable~
    </code>
     意思是“的价值
     <code>
      Variable
    </code>
     进入子程序“。
  </p>
  <P>
    我怕我不知道是什么
     <code>
      S~[Pointer=>X]
    </code>
     手段;也许是“
     <code>
      Pointer
    </code>
    的元素
     <code>
      S
    </code>
     现在是X“（如何指定所有其他元素
     <code>
      S
    </code>
     是不变？）。
  </p>
  <P>
    几点：
  </p>
  <UL>
    <LI>
      这是SPARK2014符号的不寻常混合（
       <code>
        with SPARK_Mode;
      </code>
      ）和旧式注释（
       <code>
        --#
      </code>
      ）。我想知道新的SPARK软件（
       <code>
        gnatprove
      </code>
      ）需要第一个才能识别第二个，但看起来更像是从旧到新的转换的中间阶段。
    </LI>
    <LI>
       <code>
        Pointer
      </code>
       对于显然是数组索引的东西来说，这是一个愚蠢的名称。也许
       <code>
        Top
      </code>
       会减少误导。
    </LI>
  </UL>
</DIV>

2# 真不错 | 2019-08-31 10-32