問題タブ [spark-ada]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
frama-c - C/frama-c と Spark-ada の同等性
私はフレームワーク Frama-c を研究していますが、C/Frama-c と Spark Ada の間に同等性があるかどうか疑問に思っています。このような異なる言語を比較するのは非常に奇妙に思えるかもしれませんが、David A. Wheeler の記事、Johannes Kanig の比較、および SPARK のユーザーマニュアルを少し読んだ後、SPARK と C/Frama-c/ACSL が与えるかどうかを推測するのに苦労しています。同じ証明の堅牢性と同じコードの信頼性。
あなたの視点/経験を与えてくれてありがとう！
PS: 私は frama-c を初めて使用し、SPARK プログラミングについてあまり知りません。
ada - 事後条件の意味
このコードの事前条件の意味と目的は理解できますが、事後条件の意味と目的を理解するのに問題があります。このPush部分は、整数をプッシュした後にポインタを増やすことを知っています（ Pointer = Pointer~ +1 ）。このPop部分は、整数をポップした後にポインターを減らすことを理解しています（ポインター=ポインター〜-1）。
ada - Ada spark - --# 派生句を追加
私はこの手順に派生句を追加しようとしていますが、これが私の解決策です:
--# Key から Index、Data & Found から Data および I から Data を導出します。
私はそれについて確信が持てず、助けが必要です