标签: spark-2014

Spark的新手,Ada的新手,所以这个问题可能过于宽泛.然而,作为尝试理解Spark的一部分,它是出于善意的要求.除了下面问题的直接答案,我欢迎对风格,工作流程等的批评.

作为我第一次涉足Spark,我选择尝试实现(简单)并证明正确性(迄今为止不成功)的功能 .

问题:实现和证明此功能正确性的正确方法是什么？

我从以下开始util.ads:

package Util is
   function Floor_Log2(X : Positive) return Natural with
     Post => 2**Floor_Log2'Result <= X and then X < 2**(Floor_Log2'Result + 1);    
end Util;

我没有先决条件,因为输入的范围完全表达了唯一有趣的前提条件.我根据数学定义写的后置条件; 但是,我在这里有一个紧迫的问题.如果X是Positive'Last,则2**(Floor_Log2'Result + 1)超过Positive'Last和Natural'Last.我已经在这里反对我对Ada的有限知识了,所以:子问题1:后置条件中子表达式的类型是什么,这是溢出问题吗？有没有一般解决方法？为了避免在这种特殊情况下的问题,我将规范修改为不太直观但等效:

package Util is
   function Floor_Log2(X : Positive) return Natural with
     Post => 2**Floor_Log2'Result <= X and then X/2 < 2**Floor_Log2'Result;
end Util;

有很多方法可以实现这个功能,我现在并不特别关注性能,所以我对它们中的任何一个都很满意.我认为"自然"实现(鉴于我的特定C背景)如下所示util.adb:

package body Util is
   function Floor_Log2 (X …

我正在将我在 Dafny 中做的一项练习翻译成 SPARK，其中验证尾递归函数与递归函数。Dafny 源代码（经过审查，因为它可能仍用于类）：

function Sum(n:nat):nat 
    decreases n
{ 
    if n==0 then n else n+Sum(n-1)
}

method ComputeSum(n:nat) returns (s:nat) 
    ensures s == Sum(n) 
{
    s := 0;
    // ...censored...
}

到目前为止我在 SPARK 中得到了什么：

function Sum (n : in Natural) return Natural
is
begin
   if n = 0 then
      return n;
   else
      return n + Sum(n - 1);
   end if;
end Sum;

function ComputeSum(n : in Natural) return Natural
  with
    Post => ComputeSum'Result = Sum(n)
is
   s : Natural …

代码如下所示：

规格：

type Some_Record_Type is private;

procedure Deserialize_Record_Y(Record: in out Some_Record_Type)
with Post => (
    if Status_OK then (
        ...
        other postconditions
        ...
        and then
        Record_Field_X_Count(Record) = Record_Field_X_Count(Record'Old)
        and then
        Record_Field_X(Record) = Record_Field_X(Record'Old)
    )
);

function Record_Field_X(Record: Some_Record_Type) return X_Unbounded_Array_Type;
function Record_Field_X_Count(Record: Some_Record_Type) return Natural;

身体：

type Some_Record_Type is
   record
      X_Count: Natural;
      X      : X_Bounded_Array_Type;
      Y_Count: Natural;
      Y      : Y_Bounded_Array_Type;
      ...
   end record;

function Record_Field_X(Record: Some_Record_Type) return X_Unbounded_Array_Type
is (
   ...
   a bit of logic based on values of other …

我的类型类似于:

type ID is new String (1 .. 7);
-- Example: 123-456

如何使用Ada或SPARK在代码中指定该格式？

我在考虑Static_Predicate,但是字符串必须以3个正整数开头,然后是破折号后跟另一组3个正整数的条件不能用Static_Predicate表达式来描述.