# Guards in a nutshell

This chapter presents succinctly the different kinds of guards that are available to write mathematical rules (for further details, see Appendix C). For each guard, the following elements are presented:

* syntax,
* possibly its semantics,
* a textual description of its behaviour.

It must be noted that certain guards have a mathematical semantics only under special circumstances (e.g. the bsearch guard).

The following guards may be employed to obtain one or several hypothesis from the stack, by processing first the most recently inserted hypothesis.

| Syntax        | Semantics |
| ------------- | --------- |
| bgetallhyp(H) | H         |
| bgethyp(H)    | H         |
| binhyp(H)     | H         |

The following guard checks if s is an element of STRING.

| Syntax     | Semantics  |
| ---------- | ---------- |
| bstring(s) | s : STRING |

The following guard checks if P is a conjunction.

| Syntax               | Semantics     |
| -------------------- | ------------- |
| bpattern(P, (Q & R)) | P <=> (Q & R) |

The bsearch guard has a mathematic semantics when the list in which the search is performed is the argument list of an associative and commutative operator. This is the case for the operators &, or, / and /. This is also the case of the operator , (comma) for a list of quantified variables. One must thus check that the application of the rule remains within such cases.

| Syntax                  | Semantics             |
| ----------------------- | --------------------- |
| bsearch(N, (P, Q), M)   | (P, Q) = (M, N)       |
| bsearch(N, (P & Q), M)  | (P & Q) <=> (M & N)   |
| bsearch(d, (a or b), c) | (a or b) <=> (c or d) |
| bsearch(d, (a / b), c)  | a / b = c / d         |
| bsearch(d, (a / b), c)  | a / b <=> c / d       |

The following guard succeeds if t is true and has the form a op b.

| Syntax   | Semantics |
| -------- | --------- |
| btest(t) | t         |

The following guard checks if n is a numeric value both positive and smaller or equal to maxint.

| Syntax      | Semantics |
| ----------- | --------- |
| n : NATURAL |           |

The following guard succeeds if both arguments succeed.

| Syntax     | Semantics                         |
| ---------- | --------------------------------- |
| band(P, Q) | Semantics of P and semantics of Q |

The role of the following guards is to verify the relationship between wildcards representing variables and wildcards representing expressions.

| Syntax          | Semantics  |
| --------------- | ---------- |
| bvrb(x)         | x          |
| blvar(x)        | x          |
| x P             | x (if x P) |
| bfresh(x, P, y) | y (if y P) |

##


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://b-method.gitbook.io/training-resources-for-atelier-b/guides-and-tutorials/applying-the-b-method/mathematical-proof/writing-mathematical-rules/guards-in-a-nutshell.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.