Skip to content

Commit 99ff8ce

Browse files
rcosta358rcosta358
committed
Change Concepts to Annotations
1 parent de8249f commit 99ff8ce

File tree

8 files changed

+36
-36
lines changed

8 files changed

+36
-36
lines changed

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
---
2-
title: External Refinements
3-
parent: Concepts
2+
title: "@ExternalRefinementsFor"
3+
parent: Annotations
44
nav_order: 4
5-
permalink: /concepts/external-refinements/
5+
permalink: /annotations/external-refinements-for/
66
description: Learn how to refine external libraries that cannot be annotated directly.
77
---
88

9-
# External Refinements
9+
# @ExternalRefinementsFor
1010

1111
External refinements let you add refinements to an existing class that you cannot modify.
1212

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
---
2-
title: Ghosts
3-
parent: Concepts
2+
title: "@Ghost"
3+
parent: Annotations
44
nav_order: 5
5-
permalink: /concepts/ghosts/
5+
permalink: /annotations/ghost/
66
description: Learn how to track logical state that helps express and verify richer object invariants.
77
---
88

9-
# Ghosts
9+
# @Ghost
1010

1111
Some protocols need more than a small set of named states. LiquidJava supports ghost variables for tracking extra state. They can be used in refinements and state refinements to express richer invariants about an object. Like states, ghosts are functions that take the refined object as a parameter.
1212

‎pages/annotations/index.md‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
---
2+
title: Annotations
3+
nav_order: 2
4+
has_children: true
5+
has_toc: false
6+
permalink: /annotations/
7+
description: Learn the different annotations in LiquidJava for writing specifications.
8+
---
9+
10+
# Annotations
11+
12+
LiquidJava extends Java with logical predicates and object protocol specifications. This section covers the different annotations for writing specifications.

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
---
2-
title: Refinement Aliases
3-
parent: Concepts
2+
title: "@RefinementAlias"
3+
parent: Annotations
44
nav_order: 2
5-
permalink: /concepts/refinement-aliases/
5+
permalink: /annotations/refinement-alias/
66
description: Learn how to reuse common refinement predicates with aliases to keep contracts shorter and easier to maintain.
77
---
88

9-
# Refinement Aliases
9+
# @RefinementAlias
1010

1111
When the same refinement appears repeatedly, you can define it once with `@RefinementAlias` and reuse it inside other refinements.
1212

pages/concepts/refinement-predicates.md renamed to pages/annotations/refinement-predicates.md

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
---
2-
title: Refinement Predicates
3-
parent: Concepts
2+
title: "@RefinementPredicate"
3+
parent: Annotations
44
nav_order: 6
5-
permalink: /concepts/refinement-predicates/
5+
permalink: /annotations/refinement-predicate/
66
description: Learn how to declare custom ghost functions and how they relate to ghosts and states.
77
---
88

9-
# Refinement Predicates
9+
# @RefinementPredicate
1010

1111
LiquidJava also supports a more general mechanism for declaring ghost functions, through the `@RefinementPredicate` annotation. This is a more flexible but less user-friendly way to declare ghosts. It allows declaring any ghost function with an explicit signature.
1212

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
---
2-
title: Refinements
3-
parent: Concepts
2+
title: "@Refinement"
3+
parent: Annotations
44
nav_order: 1
5-
permalink: /concepts/refinements/
5+
permalink: /annotations/refinement/
66
description: Learn about how to use refinements to specify constraints on variables, fields, parameters, and return values.
77
---
88

9-
# Refinements
9+
# @Refinement
1010

1111
In LiquidJava, refinements allow you to express restrictions as logical predicates over basic types. They let you restrict the values that a variable, field, parameter, or return value can have, which helps catch bugs before the program runs.
1212

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
---
2-
title: State Refinements
3-
parent: Concepts
2+
title: "@StateRefinement"
3+
parent: Annotations
44
nav_order: 3
5-
permalink: /concepts/state-refinements/
5+
permalink: /annotations/state-refinement/
66
description: Learn how to model protocol-oriented object states and valid method transitions.
77
---
88

9-
# State Refinements
9+
# @StateRefinement
1010

1111
Beyond basic refinements, LiquidJava supports object state modeling through typestates. This lets you describe when a method can or cannot be called based on the state of the object.
1212

‎pages/concepts/index.md‎

Lines changed: 0 additions & 12 deletions
This file was deleted.

0 commit comments

Comments
 (0)