問題タブ [spark-ada]

私はSPARKアプローチでAdaの自動列車保護を行っています。これはSPARKでの私の仕様です：

これが私のエイダです：

関数Read_Sensor_MajorityでState（1）またはState（）配列値を使用できない理由を知りたいです。それらを使用する方法がある場合、それを実現するためにSPARKの仕様に何かを入れる必要がありますか？

表示されているエラーは次のとおりです。

学校のプロジェクトでは、SPARK プログラミング言語に関する論文を書かなければなりませんが、その一部は、整数 n を取り、1 から n までの平方和を出力する短いプログラムを作成することです。C++ では、プログラムは次のようになります。

私は SPARK にまったく詳しくありません。Ada で同様のプログラムを見つけて少し修正したので、double ではなく整数で動作し、結果 (55) を出力します。

問題は、この Ada プログラムを SPARK プログラムにする方法です。Ada.Text_IO を Spark_IO に変更しようとしましたが、IDE (GPS) で「file spark_io.ads」が見つかりませんでした。また、プログラムは、例のように 5 だけでなく、任意の整数 n でも動作するはずです。よろしくお願いします。

I am very new to Ada/SPARK. I was trying to follow some tutorials from here --

http://docs.adacore.com/spark2014-docs/html/ug/gnatprove.html

Suppose I am running the ISQRT example given here (http://docs.adacore.com/spark2014-docs/html/ug/gnatprove.html#id19). All the codes (*.ads and *.adb) are bundled as a project called isqrt.gpr and the command that I am running is --

:~$ gnatprove -gnato13 -P isqrt.gpr

and the output I am getting is --

The tutorial says I need to supply a switch called -gnato13 to the prover so that it will skip some of the overflow checks., but apparently this switch is not acceptable.

any idea?

コーディングは好きではありませんが、Ada はとても好きで、まったくの初心者です。これらの点を明確にしていただけますか？

単一のスレッド化されていない CPU を搭載したコンピューターを使用している場合でも、タスクはシングル CPU のままです。もちろん、同じことがC または C++ でのforkにも当てはまります。

質問: このシナリオで、Ada タスクは fork よりも利点があると思いますか?

また、SPARK がタスクを禁止する理由も知りたいです (安全のためであることはわかっていますが、正確には、タスクを禁止することで安全性がどのように向上するのでしょうか)。

3 番目で最後の質問です。「安全なタスキング」(Ada で) を提供したい場合、タスク (タスク) を「安全」にするためには、タスクにどのような制限が必要になると思いますか。

ありがとうございました、