1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
// RUN: %dafny /compile:3 "%s" /compileTarget:js > "%t"
// note: putting /compileTarget:js after "%s" overrides user-provided option
// RUN: %diff "%s.expect" "%t"
// "url" is a built-in package in node, so it should be accessible to the
// test suite without further requirements on the setup.
module {:extern "url", "url"} URL {
class Url {
var host: string
var pathname: string
var search: string
}
method {:extern "parse"} Parse(address: string, b: bool) returns (u: Url)
}
method Main() {
var address := "http://localhost:8080/default.htm?year=1915&month=august&day=29";
var u := URL.Parse(address, true);
print "The address ", address, "\n";
print "has the following parts:\n";
print "host: ", u.host, "\n";
print "pathname: ", u.pathname, "\n";
print "search: ", u.search, "\n";
}
|
