[Bug] Incorrect online execution result in SPARK tutorial (2/2)
メンテナーはふだん 1 日以内に返信
まだ誰も着手していません。
評価
- 難易度
- 3/5
- 見積もり時間
- 1〜2日
- 初心者へのやさしさ
- 35/100
- issue の種類
- バグ
- 明瞭さ
- おおむね明確
- 活発さ
- 停滞
調査の方向性
Courses.Intro_To_Spark.Proof_of_Functional_Correctness の Example_08 から始め、L7-L8 を移動した後の array_util.adb のローカル実行とオンライン playground を比較します。報告された gnatprove コマンドを実行して playground の出力を調べます。オンラインとローカルの結果が一貫して意味上のエラーを特定すれば完了です。
索引モデルが issue の本文から書いたものです。
説明
In Courses.Intro_To_Spark.Proof_of_Functional_Correctness.Example_08:
I tried moving L7-L8 in array_util.adb to the end of if-else which should be an obvious semantic error to be fixed.
However, the online playground complains:
Local execution, on the other hand, completes without any problem:
> gnatprove -P main.gpr --checks-as-errors --level=0 --no-axiom-guard --report=all
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
main.adb:6:30: warning: array aggregate using () is an obsolescent syntax, use [] instead [-gnatwj]
6 | A : constant Nat_Array := (1, 1, 2);
| ^~~~~~~~
main.adb:7:30: warning: array aggregate using () is an obsolescent syntax, use [] instead [-gnatwj]
7 | B : constant Nat_Array := (2, 1, 0);
| ^~~~~~~~
main.adb:8:04: warning: constant "R" is not referenced [-gnatwu]
8 | R : constant Nat_Array (1..3) := Max_Array (A, B);
| ^ here
array_util.adb:6:07: info: range check proved
array_util.adb:6:34: info: length check proved
array_util.adb:10:24: info: index check proved
array_util.adb:13:25: info: index check proved
array_util.adb:15:33: info: loop invariant preservation proved
array_util.adb:15:33: info: loop invariant initialization proved
array_util.adb:16:40: info: index check proved
array_util.adb:16:61: info: index check proved
array_util.adb:16:68: info: index check proved
array_util.ads:9:14: info: postcondition proved
array_util.ads:10:34: info: index check proved
array_util.ads:10:55: info: index check proved
array_util.ads:10:62: info: index check proved
> gnatprove --version
SPARK Pro 23.0w (20220412)
Why3 for gnatprove version 1.4.1+git
alt-ergo: Alt-Ergo version 2.4.0
colibri: Colibri 2020.9
cvc4: This is CVC4 version 1.8
z3: Z3 version 4.8.15 - 64 bit
- 主要言語
- Ada
- スター
- 117
- フォーク
- 49
- 平均マージ
- 1時間 36分
- マージ済み PR（30日）
- 10
環境構築
- Dockerfile・Docker Compose ファイルなし
- プルリクエストのテンプレートなし
- コントリビューションガイドを読む
はじめの一歩
- issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
- 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
- リポジトリをフォークし、ブランチを切って変更します。
- issue 番号を参照したプルリクエストを送ります。
AdaCore/learn のほかの issue
-
question
難易度 4/5 3〜5日 初心者へのやさしさ 35/100
メンテナーはふだん 1 日以内に返信
-
難易度 1/5 1時間未満 初心者へのやさしさ 35/100
メンテナーはふだん 1 日以内に返信
-
難易度 4/5 3〜5日 初心者へのやさしさ 45/100
メンテナーはふだん 1 日以内に返信
-
Inconsistent content between "Verification Method" and "Notes"再び着手できるかも @frank-at-adacore が 873 日前に担当しましたが、オープン中のプルリクエストはありません。 オープン
AdaCore/learn#1041 · コメント 1 件 · 担当者 1 名 ·
メンテナーはふだん 1 日以内に返信
-
難易度 4/5 3〜5日 初心者へのやさしさ 35/100
メンテナーはふだん 1 日以内に返信
似ている issue
-
sync-en
難易度 1/5 1〜3時間 初心者へのやさしさ 88/100
メンテナーはふだん 2 日以内に返信
-
external
難易度 2/5 1〜3時間 初心者へのやさしさ 68/100
langchain-ai/docs#6255 ·
メンテナーはふだん 1 日以内に返信
-
detectors enhancement good first issue
難易度 2/5 1〜3時間 初心者へのやさしさ 86/100
SM260845/readme-gen#1 ·
-
難易度 2/5 1〜3時間 初心者へのやさしさ 88/100
angular/angularfire#3774 ·
メンテナーはふだん 2 日以内に返信
-
good first issue help wanted opensource september
難易度 1/5 1時間未満 初心者へのやさしさ 88/100