mirror of
https://github.com/microsoft/monaco-editor.git
synced 2025-12-22 18:32:56 +01:00
Minor tweaks to PR #1309
This commit is contained in:
parent
4c2b07fb31
commit
c35fbebb5a
1 changed files with 4 additions and 4 deletions
|
|
@ -816,7 +816,7 @@ return {
|
||||||
// Hint: Your program does not have to compute the sum and
|
// Hint: Your program does not have to compute the sum and
|
||||||
// max of the array, despite the suggestive names of the
|
// max of the array, despite the suggestive names of the
|
||||||
// out-parameters.
|
// out-parameters.
|
||||||
method M(N: int, a: array‹int›) returns (sum: int, max: int)
|
method M(N: int, a: array<int>) returns (sum: int, max: int)
|
||||||
requires 0 <= N & a != null & a.Length == N;
|
requires 0 <= N & a != null & a.Length == N;
|
||||||
ensures sum <= N * max;
|
ensures sum <= N * max;
|
||||||
{
|
{
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue