Nantes B Libraries Page  (Etude de cas : Video shop en B) sdssssssscbvcbvsssslhkhhkjhkjhkjhkhkjkjhkssssssdsdsdsdsdsdsdsdsdssd

Dans le cadre du mini-projet du DESS, on va s'appuyer sur l'étude de cas "video shop", déjà traité en $Z$ dans le module D2.

Bref rappel du cahier de charges
Un club vidéo a des membres qui peuvent louer des vidéos et des employés qui sont responsables de l'enregistrement des transactions du club.
Les membres peuvent louer des vidéos s'ils ont l'âge requis. Pour cette raison le club a besoin d'enregistrer leur date de naissance. Il enregistre aussi les adresses des membres de façon à engager des actions appropriées lorsque des vidéos louées ne sont pas rendues.
Les employés du club peuvent aussi louer des vidéos. Les vidéos  sont classés sur les étagères selon les sujets (horreur, comédie, X, etc). Chaque vidéo a un tarif de location qui dépend de sa popularité (courante) et du fait qu'il soit récent.
Il n'y a que très peu de tarifs qui s'appliquent à tout moment.

Modélisation en $B$ du système de location
Le cahier de charges sera analysé et précisé au fur et à mesures.
On donnera une spécification $B$ complète et on analysera formellement cette spécification en utilisant l'$Atelie B$.  Certaines parties doivent être raffinées jusqu'à la génération de code en C.

Références
 Z in Practice, R. Bardin, S. Stepney, D. Cooper,  Prentice Hall.