Skip to content

Commit 5b2e01f

Browse files
rcosta358rcosta358
committed
Refactor Pages
1 parent a63412a commit 5b2e01f

File tree

15 files changed

+13
-3
lines changed

15 files changed

+13
-3
lines changed

concepts/external-refinements.md renamed to pages/concepts/external-refinements.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22
title: External Refinements
33
parent: Concepts
44
nav_order: 4
5+
permalink: /concepts/external-refinements/
56
---
67

78
# External Refinements
@@ -39,4 +40,3 @@ Socket socket = new Socket();
3940
socket.connect(new InetSocketAddress("example.com", 80)); // type error!
4041
socket.close();
4142
```
42-

concepts/ghosts.md renamed to pages/concepts/ghosts.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22
title: Ghosts
33
parent: Concepts
44
nav_order: 5
5+
permalink: /concepts/ghosts/
56
---
67

78
# Ghosts
@@ -44,4 +45,3 @@ In the `push` method, we specify no precondition, since we can always push an el
4445
In the `pop` method, we specify a precondition that the `size` must be greater than zero, since we cannot pop from an empty stack. We also specify a postcondition that decrements the `size` by one, similarly to the `push` method.
4546

4647
In the `peek` method, we specify the same precondition, since we also cannot peek from an empty stack, but we don't specify a postcondition since peeking does not change the size of the stack.
47-

concepts/index.md renamed to pages/concepts/index.md

File renamed without changes.

concepts/refinement-aliases.md renamed to pages/concepts/refinement-aliases.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22
title: Refinement Aliases
33
parent: Concepts
44
nav_order: 2
5+
permalink: /concepts/refinement-aliases/
56
---
67

78
# Refinement Aliases

concepts/refinements.md renamed to pages/concepts/refinements.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22
title: Refinements
33
parent: Concepts
44
nav_order: 1
5+
permalink: /concepts/refinements/
56
---
67

78
# Refinements

concepts/state-refinements.md renamed to pages/concepts/state-refinements.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22
title: State Refinements
33
parent: Concepts
44
nav_order: 3
5+
permalink: /concepts/state-refinements/
56
---
67

78
# State Refinements

diagnostics/custom-messages.md renamed to pages/diagnostics/custom-messages.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22
title: Custom Messages
33
parent: Diagnostics
44
nav_order: 3
5+
permalink: /diagnostics/custom-messages/
56
---
67

78
# Custom Messages

diagnostics/errors.md renamed to pages/diagnostics/errors.md

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22
title: Errors
33
parent: Diagnostics
44
nav_order: 1
5+
permalink: /diagnostics/errors/
56
---
67

78
# Errors
@@ -20,4 +21,4 @@ An error can be caused by a refinement violation, an invalid refinement, or anot
2021
| `InvalidRefinementError` | A refinement is semantically invalid, such as a non-boolean expression |
2122
| `CustomError` | Any other error, such as providing a non-existent path to verify |
2223

23-
LiquidJava is only able to report **at most one error per method** to avoid cascading failures. If there are multiple errors in a method, the verifier will report the first one it encounters, and stop verifying the rest of the method, meaning that fixing one error can sometimes reveal another that was previously hidden.
24+
LiquidJava is only able to report **at most one error per method** to avoid cascading failures. If there are multiple errors in a method, the verifier will report the first one it encounters, and stop verifying the rest of the method, meaning that fixing one error can sometimes reveal another that was previously hidden.

diagnostics/index.md renamed to pages/diagnostics/index.md

File renamed without changes.

diagnostics/understanding-refinement-errors.md renamed to pages/diagnostics/understanding-refinement-errors.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22
title: Understanding Refinement Errors
33
parent: Diagnostics
44
nav_order: 4
5+
permalink: /diagnostics/understanding-refinement-errors/
56
---
67

78
# Understanding Refinement Errors

0 commit comments

Comments
 (0)