mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
19 lines
641 B
Plaintext
19 lines
641 B
Plaintext
digraph G {
|
|
graph [bgcolor=lightgray; rankdir="TB"];
|
|
node [margin=0.05,shape=ellipse,style=filled,fillcolor="cyan"];
|
|
"entry" [pos="2,3!"];
|
|
"L" [pos="2,2!"];
|
|
"invariant" [pos="2,1!"];
|
|
"cond" [pos="2,0!"];
|
|
"do" [pos="0,1!"];
|
|
"exit" [pos="4,0!"];
|
|
|
|
"entry" -> "L" [label=" i <- 0"];
|
|
"L" -> "invariant" [label=" m <- a[i]"];
|
|
"invariant" -> "cond" [label=" i <- i+1"];
|
|
"cond" -> "exit" [label=" i >= n"];
|
|
"cond" -> "do" [label=" i < n"];
|
|
"do" -> "L" [label=" a[i] > m"; headport=e];
|
|
"do" -> "invariant" [label=" a[i] <= m"];
|
|
}
|