Skip to content

Commit b8256e1

Browse files
author
davidcok
committed
Trying navigation
1 parent 71e10c3 commit b8256e1

File tree

2 files changed

+19
-1
lines changed

2 files changed

+19
-1
lines changed

tutorial/Postconditions.md

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,21 @@
1+
<div style="display: flex; justify-content: space-between;">
2+
<div style="width: 30%; white-space: nowrap; overflow: hidden; text-overflow: ellipsis;">
3+
<a href="TOC.html">&lt;&lt;&lt;Previous</a>
4+
<br>
5+
This content will not wrap if it's too long, but it will be cut off.
6+
</div>
7+
<div style="width: 30%; white-space: nowrap; overflow: hidden; text-overflow: ellipsis;">
8+
<a href="TOC.html">TOC</a>
9+
<br>
10+
This content will also be on a single line.
11+
</div>
12+
<div style="width: 30%; white-space: nowrap; overflow: hidden; text-overflow: ellipsis;">
13+
<a href="Preconditions.html">Nexti &gt;&gt;&gt;</a>
14+
<br>
15+
Keeping things spread out across the page.
16+
</div>
17+
</div>
18+
119
---
220
title: JML Tutorial - Postconditions (ensures clauses)
321
---

tutorial/T_ensures3.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
public class T_ensures3 {
33
//@ requires a.length > 0;
44
//@ ensures \result == a[0];
5-
public int fist(int[] a) {
5+
public int first(int[] a) {
66
return a[0];
77
}
88
}

0 commit comments

Comments
 (0)