blob: 7842e5925c5e1f5dd2c7711b7819baefc9aa3f3a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
|
#include <vector>
#include <ranges>
#include <string>
#include <span>
#include <algorithm>
#include <iostream>
main: () -> int = {
insert_at( 0, 42 );
std::cout << make_string() + "plugh\n";
std::cout << make_strings().a + make_strings().b + "\n";
}
vec: std::vector<int> = ();
insert_at: (where: int, val: int)
pre ( 0 <= where && where <= vec.ssize() )
post( vec.size() == vec.size()$ + 1 )
= {
vec.push_back(val);
}
make_string: () -> (ret: std::string = "xyzzy")
post (ret.length() == ret.length()$ + 5)
= {
ret += " and ";
}
make_strings: ()
-> (
a: std::string = "xyzzy",
b: std::string = "plugh"
)
post (a.length() == b.length() == 5)
= {
// 'return' is generated when omitted like this
}
|