Table des matières

CR rapide du 16/04/09
- Travail à propos de la sémantique Kmelia
- Travail à propos de la traduction Kmelia2B
  - Fonctions
  - postconditions

CR rapide du 16/04/09

(rédigé par PA)

Présents : PA, GA, CA, MM, AL, PS

Travail à propos de la sémantique Kmelia

PS: Quelle est la prochaine analyse prévue ?

assemblage global
concurrence

Travail à propos de la traduction Kmelia2B

Fonctions

Comment déclarer des fonctions

mathématique
non
fonction (fonctionnel) –

> voir [[types_fonctions#fonctions|fonctions en kmelia]]
1. prédéfinie DEFAULT
2. use maLibrairie voir librairies kmelia
- traduction en B des fonctions Kmelia :
  1. soit via des lambda-fonctions B
  2. soit via des opérations d'une machine incluses
- syntaxe :
  - pas dans le modèle
  - dans la spec : mot-clé USE pour les librairies kmelia
- modèle TODO
  - environnement (et bibliothèques de fonctions)
  - assemblage-type
  - composant-type
=

types et B

limitations : POUR LE MOMENT pas un problème
rester expressif sinon pas mieux que CSP+

postconditions

postconditions
result
- old(var)
- tableaux
  - boucles : while (sucre pour le eLTS) limitations possibles (ex: pas de com= * initialisation rapde à définir * fonction “prédéfinie”
    ==== initialisation ==== * affectations simples ==== offert/requis ==== * contexte virtuel et/ou contrainte de “même serveur” utile à l'assemblage * AL : même contexte virtuel * PA/GA : pas obligatoire, on préfère une contrainte en plus : plus souple virtuel = * contexte = scope pour assertions * contrainte de même serveur peut se faire avec des contextes quelconques solution : uniquement des déclarations locales version 1 VirtualContext Variable Invariant version2
    virtual Variable virtual Invariant la 2 est choisie * pas de init * besoin de properties ? plus tard * requis : subrequires * nécessaire ? lourd ? ==== contrainte d'assemblage ==== * même serveur dans clause PROPERTIES r1 = _r2 ou sameprovider(r1, r2, …)