Add exercises for techniques

This commit is contained in:
engboris 2024-06-14 22:37:16 +02:00
parent 65241154a0
commit 2b48ab39dd
6 changed files with 144 additions and 19 deletions

View File

@ -38,7 +38,7 @@ peut-être lue comme "si X implique Y alors afficher ok".
# Cas d'échec
Remarquez qu'il n'est pas (nativement) possible de représenter le `else` de la
Il n'est pas (nativement) possible de représenter le `else` de la
programmation. Il est donc nécessaire de capturer tous les cas manuellement
lorsque l'on souhaite être exhaustif :

View File

@ -5,10 +5,48 @@ weight: 8
# Exercices
## Vérifications exactes
## Conditions (pseudo-)imbriquées
## Conditions imbriquées
Représenter (naïvement) la condition suivante avec une constellation de telle
sorte à ce qu'elle retourne `message(use more duct tape);` avec la constellation
`@+it_moves(1); @+it_should_move(0);` :
## Boucles imbriquées
```
if it moves and it should move
no problem
if it moves and it should not move
use more duct tape
if it does not move and it should move
use more lube
if it does not move and it should not move
no problem
```
## Branchage conditionnel
{{< details title="Solution" open=false >}}
```
-it_moves(1) -it_should_move(1) message(no problem);
-it_moves(1) -it_should_move(0) message(use more duct tape);
-it_moves(0) -it_should_move(1) message(use more lube);
-it_moves(0) -it_should_move(0) message(no problem);
@+it_moves(1);
@+it_should_move(0);
```
{{< /details >}}
{{< hint info >}}
Il n'est pas nativement possible la condition suivante :
```
if it moves
if it should move
no problem
else
use more duct tape
else
if it should move
use more lube
else
no problem
```
car cela requiert des mécanismes de liaisons séquentielles.
{{< /hint >}}

View File

@ -61,7 +61,7 @@ de boucle :
@+f(s(s(s(0))));
```
Remarque : on a ajouté une étoile `-f(0) end` pour repérer le moment où la
On a ajouté une étoile `-f(0) end` pour repérer le moment où la
boucle laisse `0` (on a retiré tous les `s`) pour ensuite produire `end` en
sortie.
@ -79,6 +79,20 @@ compteur associée :
@+f(s(s(s(0))));
```
# Exemple : addition unaire
Un exemple typique de boucle est le programme de programmation logique qui
calcule la somme d'entiers unaires :
```
+add(0 Y Y);
-add(X Y Z) +add(s(X) Y s(Z));
@-add(s(s(0)) s(s(0)) R) R; 'query
```
Ici, on calcule la somme `2+2` et on récupère le résultat dans `R`.
# Cas général
Dans cette section, nous avons seulement considéré des étoiles de boucles

View File

@ -1,12 +0,0 @@
---
title: "Permissions"
weight: 6
---
# Permissions
## Composition
## Composition conditionnée
(soon)

View File

@ -0,0 +1,40 @@
---
title: "Permissions"
weight: 6
---
# Permissions
Prenons une constellation formant un chemin entre deux étoiles :
```
-1 +2; -2 +3;
```
Imaginons que nous voulions conditionner la connexion entre `+2` et `-2` de
sorte à ce qu'elle n'arrive que sous certaines conditions.
Il est impossible de placer un intermédiaire qui viendrait perturber la
connexion déjà existante. Si on essaie d'ajouter une autre occurrence de `+2` ou
de `-2` dans une autre étoile, on aura une connexion *en plus* (duplication) et
non *à la place* de la précédente.
On peut modifier la constellation comme suit :
```
-1 +2(a); -2(b) +3; -2(a) +2(b);
```
Le chemin passe maintenant par un intermédiaire `-2(a) +2(b);` auquel on peut
ajouter des rayons afin d'imposer des contraintes supplémentaires pour
autoriser l'usage de ce pont.
On pourrait conditionner la connexion par un booléen ou par n'importe quel autre
contrainte plus complexe et éventuellement calculée par une autre constellations
dédiée :
```
-1 +2(a); -2(b) +3; -2(a) +2(b) -bool(true);
@+bool(true)
```
De telles étoiles agissent comme des demandes de permissions pour l'interaction.

View File

@ -3,4 +3,49 @@ title: "Tests unitaires"
weight: 7
---
(soon)
# Tests unitaires
La notion de test est native dans la résolution stellaire et on l'utilise
constamment et implicitement.
Un test unitaire permet de vérifier le bon comportement d'une constellation.
Si on encode une fonction par une constellation, on pourrait la tester face à
certaines entrées représentative de son domaine.
Testons la constellation d'addition unaire :
```
+add(0 Y Y);
-add(X Y Z) +add(s(X) Y s(Z));
+test(X Y R) -add(X Y R) ok(X Y R);
@-test(0 0 0);
@-test(0 s(0) s(0));
@-test(s(0) 0 s(0));
@-test(s(0) s(0) s(s(0)));
@-test(s(s(0)) s(0) s(s(s(0))));
```
On retrouve un rayon `ok(X Y R)` pour chaque test réussi. Mais que se passe
t-il lorsqu'un test échoue ? Il n'apparaît pas car son calcul n'est pas allé
jusqu'au bout. On peut justement faire apparaître de telles étoiles avec
l'option `-allow-unfinished-computation`.
On peut aussi utiliser des variables dans les tests et effectuer des tests
*symboliques* :
```
+add(0 Y Y);
-add(X Y Z) +add(s(X) Y s(Z));
+test(X Y R) -add(X Y R) ok(X Y R);
@-test(0 X X);
@-test(s(0) X s(X));
```
C'est en général insuffisant pour tester qu'une fonction est correcte mais
cela apporte déjà une certaine confiance. La résolution stellaire fait vivre
programmes et tests dans le même espace (ils sont de même nature), ce qui nous
permet des tests plus subtils.