RÉFÉRENCE VITTE / Langage

Instructions et contrôle

Les instructions déclarent des valeurs locales, modifient l’état, contrôlent le parcours et terminent parfois une procédure.

Niveau de garantieLes instructions courantes ont des preuves runtime ; les constructions sans fixture sont indiquées comme non prouvées.
Source de référence : grammar/vitte.ebnf

Variables locales et affectation

let reponse: i64 = 42;
let mut compteur: i64 = 0;
set compteur = compteur + 1;

let peut préciser mut, un type, une valeur initiale, ou les deux. set introduit une expression d’affectation. Une liaison immuable ne doit pas être modifiée ; les règles exactes sont vérifiées lors de l’analyse sémantique.

Retour et fin de boucle

  • return expression; et give expression; renvoient une valeur ; les formes sans expression terminent une procédure sans résultat.
  • break; sort de la boucle courante.
  • continue; passe au prochain cycle de la boucle courante.

Conditions et répétitions

if pret {
    traiter();
} elif en_attente {
    patienter();
} else {
    terminer();
}

while indice < 4 {
    set indice = indice + 1;
}

for valeur in 0..4 {
    utiliser(valeur);
}

La grammaire prévoit if/elif/else, while, loop et for nom in expression. Les exemples de bibliothèque parcourent des plages demi-ouvertes : 0..4 contient 0 à 3. Les types de séquences itérables disponibles restent dépendants de l’implémentation.

Match

match etat {
    Etat.Inactif => { afficher("arrêt"); },
    Etat.Pret => { afficher("prêt"); },
}

Les bras de la grammaire ont la forme expression => bloc-ou-expression, séparés par des virgules. La production formelle accepte des expressions de bras ; ne suppose pas la prise en charge de motifs plus riches sans confirmation dans l’analyseur et le compilateur.

Assertions, différé, unsafe et assembleur

  • assert(expression); vérifie une propriété à un point donné.
  • defer expression; ou defer { ... } marque une action différée ; vérifie le moment d’exécution garanti par le compilateur ciblé.
  • unsafe { ... } délimite un bloc qui exige des garanties manuelles.
  • asm(...); et asm "..."; sont les formes d’assembleur admises par la grammaire.
La grammaire ne prouve pas la sûreté

Un bloc unsafe, une assertion ou une instruction reconnue ne garantit ni l’absence de dépassement ni le support par le backend.

Vérification par instruction

InstructionEBNFAnalyseurCompilation constatée
let, let mut, setDécrites.Acceptées ; test natif confirme aussi le rejet de set sans affectation.Oui : liaisons, mutation locale, champs et index de tableau passent l’IR/C17 et l’exécution.
return / giveLes deux formes sont décrites.return est utilisé dans toutes les suites ; fixture dédiée à give non relevée.return est largement compilé ; give non prouvé séparément.
if / elif / elseDécrites.if/else sont testés ; la parité de elif n’a pas de cas runtime retenu.Oui pour conditions et sélection de valeurs dans les fixtures runtime.
while, break, continueDécrites.Acceptées dans les fixtures d’exécution.Oui : boucles et cibles de sortie/continuation compilées et exécutées.
loopDécrite.Pas de fixture ciblée dans les suites exécutées pour cette forme exacte.Non prouvé.
for nom in expressionDécrit.La syntaxe atteint le diagnostic backend dans le cas d’un tableau.for nom in tableau est rejeté avec VITTE_BACKEND_E_CODEGEN. L’exécution d’une boucle for sur plage n’est pas prouvée par l’audit.
match simple et variantes à charge utilematch et les bras simples sont décrits ; gardes/motifs sont des extensions par rapport à l’EBNF.Acceptés dans les fixtures natives, y compris motifs de variantes et joker.Oui : IR, C17 et exécution de choix simples et à charge utile.
assertDécrite.Syntaxe listée ; pas de fixture isolée de cette instruction dans les tests runtime retenus.Non prouvé comme instruction au backend dans cet audit.
defer, unsafe, asmDécrites.Pas de fixture représentative identifiée pour chacun.Non prouvé au backend et à l’exécution.

Sources : grammaire EBNF · tests du frontend natif · liste des fixtures runtime · matrice générale.