PROSAGA码农传奇-Ada-隐含功能合同不适用于证明

隐含功能合同不适用于证明

作者: 爱我真好
发布时间: 2024-07-15 05:44:32 (21天前)
转自：

<div class =“post-text”itemprop =“text”>
  
    如果我被允许编辑
     <code>
 Sim
 </code>
     包，我可以说例如
  
   <pre class="lang-ada prettyprint-override">
 <code>
 package Sim
with SPARK_Mode
is
 function Get return Float
 with Annotate => (Gnatprove, Terminating);
end Sim;

</code>
 </pre>
  
    （那是使用AdaCore的spark2017版本），并跟进非SPARK机身
  
   <pre class="lang-ada prettyprint-override">
 <code>
 package body Sim is
 function Get return Float is (42.0);
end Sim;

</code>
 </pre>
  
    该报告显示Sim.Get已被跳过。
  
  
    SPARK2014的后期版本将如何对此做出反应我不知道，因为其含义来自于
    <a href="https://docs.adacore.com/spark2014-docs/html/ug/en/source/how_to_write_subprogram_contracts.html#subprogram-termination" rel="nofollow noreferrer">
      用户指南
    </A>
     就是它
     <code>
 Annotate
 </code>
     为证明者设定了一个目标，然而我们却不允许它进入身体
     <code>
 Sim
 </code>
     去检查。
  
  
    也许在参考手册中还有更多内容 - 访问adacore.com，选择Resources / Documentation / SPARK。
  
</DIV>