Specmanで配列を返す

Question

Specmanのメソッド呼び出しから配列を返すにはどうすればよいですか？例えば。

method a : list of uint is { 
    var data: list of uint; 
    ..... 
    result = data; 

}; 

extend sys { 
var data_sys: list of uint; 
run() is also { 
    data_sys = a(); 
}; 
}; 

一部の要素が配列データとdata_sysと異なることが示されています。私が逃したものを教えてくれませんか？

Answer 1

投稿したコードはコンパイルされません。より多くのprint文を記述するか、またはspecviewにブレークポイントを設定し、コードをステップ実行します。プリントアウトを行っているテスト段階を知っていますか？ data_sysを（Specmanに生成させる代わりに）手続き的に設定したい場合は、do-not-generate修飾子 '！'を指定する必要があります。

[...] 
!data_sys : list of uint; 
[...] 

Answer 2

のplsはsscceを提供しています。それなし

、この非常に基本的な例が行う可能性があります：

extend sys { 
    m() : list of uint is { 
    print result.size(); // result.size() = 0 
    }; 

    run() is also { 
    var m := m(); 
    }; 
}; 

方法は、デフォルトでは、あなたのために割り当てられた配列を、返すことができます。それはポインタによって返されるので、注意してください。

親指のルールとして、それらを計算する際にリストを返すメソッドは避けてください。この方法は、作成方法やゲッターでない限り、その動的な性質を伝えるために、パラメータとしてリストを渡すしよう：

collect_packets(packets : list of packet) is {...}; 
get_collected_packets() : list of packet is {...};