Introduction Le projet qui nous a été confié était de réaliser une application web de moteur de recherche de document dans une bibliothèque de livres sous format textuel. Il est grandement inspiré de la base de Gutenberg. L'idée est de proposer aux utilisateurs la possibilité de trouver et de lire des livres, parmi une grande bibliothèque (qui s'agrandit de jour en jour) qu'ils auront cherché par un/des mot(s) clef(s) ou par des expressions régulières. Nous avons donc travaillé afin d'offir à l'utilisateur une expérience agréable et intuitive (via notre système de suggestions) en plus d'une bonne réactivité (temps de recherche court). Par la suite, nous allons présenter avec précision notre architecture et détailler nos différents choix techniques faits ainsi que leurs implémentations. Architecture Notre moteur de recherche s'appuie sur une architecture en trois couches : data, serveur et client.

Spec <expéditeur>:<destinataire>:<commande>:<nbArgs>:<arg1>:<arg2>:...:<argn>:<EOF> Expéditeur : Int de n digits avec le premier digit qui est soit 1 si main bot soit 2 si secondary Destinataire : Int 0 si tout le monde sinon id du destinataire Commande : String nom de la commande (se référer à la liste plus bas) Nb Args: Int Nombre d'arguments

DAAR 20% Egrep (Oct) 20% Elastic (Nov) 20% Ethereum (Nov) 10% TME7-10 algorithmic (Dec) 30% Final project (Avril) GPSTL 10% GANTT 25% Vidéo pitch 28/11

Algèbre de processus Résumé du chapitre Les algèbres de processus sont une famille de langages formels permettant de modéliser les systèmes (informatiques) concurrents ou distribués. Les expressions du langages sont interprétés comme un système de transition étiqueté ou LTS (Labelled Transition System). Entre ces deux modèles la bisimilarité est utilisée comme une sémantique d'équivalence. Syntaxe et représentations graphiques Le langage CCS a été créé en 1980 et sert à décrire des processus parallèle. Sa syntaxe est : $$

@gnouf @nlejeune https://hal.archives-ouvertes.fr/hal-00469007v4/document NARDIN Théo LEJEUNE Nicolas Cadre de recherche $\hspace{0.5cm}$Le développement de systèmes embarqués nescessitent l'utilisation du concept de Model-Based design, c'est à dire le fait de répliquer le comportement réel d'un modèle. Pour répéter la réalité au plus proche, le système a besoin d'une précision chirurgicale, chose qui ne lui est pas apportée par le fonctionnement classique des nombres flottants.

Lambda Légendes : :skull_and_crossbones: Mort :heavy_check_mark: Vivant Casual: 0,5 Secondary 0,75 Main

@mamy @theOnlyAlex @wlin @nlejeune @gnouf Exercice 1 { int i; int v; v = rand(0, 3); while(i < 4) { i = i + 1; v = 3 * v + 1;

@mamy @theOnlyAlex @wlin @nlejeune @gnouf Question 1 $[0, 4] \leq^# [1, 3] = [0, 3], [1, 3]$ $[1, 3] \leq^# [0, 4] = [1, 3], [1, 4]$ $[0, 2] \leq^# [3, 5] = [0, 2], [3, 5]$ $[3, 5] \leq^# [0, 2] = \bot, \bot$ Question 2

Fonctionalités minimales Tirer sur une cible en mouvement Détecter la position d'une cible Partager la position d'une cible (en temps réel) Avancer en tirant Mouvements d'esquive pendant la recharge de balle Changer de priorité de cible par rapport à la distance des cibles Fonctionalités avancées

@mamy @theOnlyAlex @wlin @nlejeune @gnouf Cours Décomposition Modulaire : http://www.lirmm.fr/~paul/lecture1-MD.pdf Abstract (traduction littérale) Un graphe temporel G est une séquence de graphes statiques indexés par un ensemble d'entiers T représentant les instants temporels. Pour $\Delta$ un entier, une paire de $\Delta$-jumeaux est une paire de sommets $u \neq v$ pour lesquels, à partir d'un certain instant, ont exactement les mêmes voisins hors ${u, v}$ pour chaque instants $\Delta$ consécutifs. Nous abordons le problème d'énumération de toutes les paires de $\Delta$-jumeaux dans G, tel que le temps global dépende le moins de la longueur de l'historique, à savoir : $$ max{t : G_t \in G\ non\ vide } - min {t: G_t \in G\ non\ vide} $$

@mamy @theOnlyAlex @wlin @nlejeune @gnouf Exercice 1 $$ \mathbb{S}(\gamma[stnt]) \subseteq \gamma (\mathbb{S}[stnt]),\ \forall\ S^#,\ \forall\ stnt. $$ $$ S^# \sqsubseteq \mathbb{C}[[bexpr]] S^# \

@mamy @theOnlyAlex @wlin @nlejeune @gnouf raphael.monat@lip6.fr $$E = v \to P(\mathbb{Z})$$ $$ \mathbb{E}[[rand(a, b)]]: E \to P(\mathbb{Z}) \ \mathbb{E}[[rand(a, b)]] \rho = { x | a \leq x \leq b} $$

@nlejeune @gnouf Liens utiles https://github.com/garethbjohnson/gutendex $\to$ gutenberg-project's API Tâches Base De Données [ ] ER Diagram (Datagrip)

[TOC] Lambda calcul Expressions $$ E := E ;\text{(Var)};|; \lambda x.E;\text{(Abs)} ;|; E1;E2;\text{(App)} $$ Beta-reduction ($\rightarrow_\beta$) Une manière de voir les termes du lambda-calcul consiste à les concevoir comme des arbres ayant des nœuds binaires (les applications), des nœuds unaires (les λ-abstractions) et des feuilles (les variables).

Exercice Surcharge : class A { void m(B x) { /* A1 */ } void m(C x, B y) { /* A2 */ } } class B extends A { void m (A x) { /* B1 */} void m (B x , A y) { /* B2 */ } void m (C x , B y) { /* B3 */ } }

Pense-bête $\lceil log(a)\rceil \leq log(a) + 1$ Nombre de Stirling $\to n! \approx \sqrt{2\pi . n}\ \lgroup{\frac{n}{e}\rgroup^n}$ $\sum_{i=1}^{n} 1\ + 2\ + 3\ + ...\ + n = \frac{n\ (n + 1)}{2} \to \frac{(dernier\ terme)\ \times\ (nombre\ de\ termes)}{2}$ Génération d'entiers Les deux types de générateurs d'entiers sont : True Random Number Generators : Utilisés en crypto et assez complexe à réaliser. Il sont souvent basés sur des données physique extérieure.

(Proposition par @gnouf ) Groupes Groupes réalisés aléatoirement à l'aide de random.org Groupe 1 Sujet A chill -> Création correction Sujet B partiel blanc -> Utilisation de la correction de l'autre groupe @mamy (Plus tout seul :man-with-bunny-ears-partying: )

Notions présentes dans l'examen Réduction de processus Modélisation en $\pi$-calcul Bisimilarité Types simples Expression en $\pi$-calul typable ou pas Types sangiorgi

@theOnlyAlex @sroFAHGMRJaJlDo7cVYdbw Lien : https://plv.mpi-sws.org/refinedc/paper.pdf Gilab du projet a priori : https://gitlab.mpi-sws.org/iris/refinedc Glossaire Preuve fondamentale : Preuve automatique :

Glossaire IRIS : Iris est un framework qui peut être utilisé pour raisonner sur la sécurité des programmes concurrents, comme la logique des relations logiques, pour raisonner sur les systèmes de types, l'abstraction de données, etc. Coq : Coq est un assistant de preuve qui permet à son utilisateur de construire des démonstrations de façon semi-automatique, tout en garantissant la correction de ces démonstrations. Ce type d'outil est utile à la vérification de logiciel critique. Coq est l'un des outils de ce type les mieux considéré. Contexte Bien que le C ait été créé en 1972 de nombreux systèmes critiques ont été développés et surtout sont toujours développés dans ce langage. La raison de ce choix vient de l'important contrôle qu'offre le C sur la mémoire de la machine permettant une optimisation très fine de cette dernière. Néanmoins ce contrôle excercé par le développeur est aussi une source importante de bug grave pouvant toucher des systèmes particulièrement important. En effet le langage C est utilisé aujourd'hui pour de nombreuses applications critiques comme les systèmes d'exploitations ou les compilateurs et interpréteurs comme celui de python. Des générations de chercheurs et d'ingénieurs ont donc cherché a avoir des outils permettant de réduire les risques que de tel problèmes arrivent et ReffinedC est l'un de ces outils. ReffinedC a donc été créé pour répondre a une simple question : Ce code source en C est t-il fiable ?