Skip to content

Commit

Permalink
Fix coding style in contracts.dd
Browse files Browse the repository at this point in the history
  • Loading branch information
H. S. Teoh committed Aug 23, 2014
1 parent ac8eed8 commit 7a99266
Showing 1 changed file with 18 additions and 15 deletions.
33 changes: 18 additions & 15 deletions contracts.dd
Original file line number Diff line number Diff line change
Expand Up @@ -157,13 +157,14 @@ $(H2 Invariants)
------
class Date
{
int day;
int hour;

invariant() {
assert(1 <= day && day <= 31);
assert(0 <= hour && hour < 24);
}
int day;
int hour;

invariant()
{
assert(1 <= day && day <= 31);
assert(0 <= hour && hour < 24);
}
}
------

Expand Down Expand Up @@ -195,14 +196,16 @@ class Date
)

------
class Foo {
public void f() { }
private void g() { }

invariant() {
f(); // error, cannot call public member function from invariant
g(); // ok, g() is not public
}
class Foo
{
public void f() { }
private void g() { }

invariant()
{
f(); // error, cannot call public member function from invariant
g(); // ok, g() is not public
}
}
------

Expand Down

0 comments on commit 7a99266

Please sign in to comment.