Boogie
1 program
Added 2025-10-28T10:37:37Z
Model: x-ai/grok-4-fastTemp: 0.4
Evidence
Report issue
View issues
Aliases: —
Provenance: commit 0f0efa8c53 · authored 2025-10-28T11:37:37+01:00 · model x-ai/grok-4-fast
Sources mentioning this language
4 sources · pl_id:
pl/boogieExtensions claimed by this language
2 claims. Each row is one upstream assertion with its strength.
SWH column shows file occurrences with that extension across the entire archive.| Extension | Source | Strength | SWH |
|---|---|---|---|
.bpl | linguist | primary | 112.8K files |
.bpl | pygments | primary | 112.8K files |
Related languages
LLM-contributed programs
Zeroing the first array element verification example
Provenance: commit 0f0efa8c53 · authored 2025-10-28T11:37:37+01:00 · model x-ai/grok-4-fast · Temp 0.4
// Simple example: Zeroing the first array element
function Sum(A: [int]int, B: int, E: int) returns (s: int)
requires B <= E;
ensures s == (if B == E then 0 else A[B] + Sum(A, B+1, E));
{
if (B == E) then 0 else A[B] + Sum(A, B+1, E)
}
procedure ZeroFirst(A: [int]int, m: int, n: int) returns (A': [int]int)
requires 0 <= m && m < n;
requires (forall i: int :: 0 <= i && i < n ==> A[i] >= 0);
ensures (forall i: int :: 0 <= i && i < n ==> A'[i] == if i == 0 then 0 else A[i]);
ensures Sum(A', 0, n) == Sum(A, 1, n);
{
A' := A[0 := 0];
}Real programs from Software Heritage
No SWH evidence indexed yet for this language. (Either the SWH mining hasn't reached this language's extensions, or no matching files exist in the archive.)