Instructions

This commit is contained in:
Denis Merigoux 2020-03-08 06:54:35 +01:00
parent c4ff3a18e9
commit 6c0097e12e
4 changed files with 18 additions and 428 deletions

View File

@ -1,11 +1,9 @@
# Verifisc
# Lawspec
Verifisc is a low-level intermediate representation designed to be a common target
for languages and DSL describing legal specifications. The goal is to run different
passes of abstract interpretation and symbolic execution on Verifisc, or to translate
it directly to Z3 in order to gain insight on the legislation that the code describes.
Lawspec is a domain-specific language for deriving faithful-by-construction algorithms
from legislative texts.
## Usage
## Installation
The project is distributed as a Dune artifact. Use standard dune commands to build
and install the library. In particular, if you want to install the library as an opam
@ -13,6 +11,20 @@ package, use the following command at the root of the repository:
opam install ./
You can then can the compiler using the `lawspec` command.
## Usage
Use `lawspec --help` to get more information about the command line options available.
## Test
In the `test` folder, you will find the `allocations_familiales.lsp` file which contains the
algorithm computing French family benefits. The algorithm consists of annotations to the legislative
texts that define the family benetifs, using the literate programming paradigm. The `lawspec`
compiler can extract from the `.lsp` file a lawyer-readable version of the annotated text.
To get that lawyer-readable version (which is a LaTeX-created) PDF, use `make test` at the root of
the repository, and then use `make` inside ghe `test` directory to compile the LaTeX file.
## License

View File

@ -1,8 +0,0 @@
*.aux
*.dvi
*.fdb_latexmk
*.fls
*.log
*.out
*.fls
allocations_familiales.pdf

View File

@ -1,2 +0,0 @@
watch:
latexmk -pdf -pvc -halt-on-error -shell-escape allocations_familiales.tex

View File

@ -1,412 +0,0 @@
\documentclass[11pt, french]{article}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{lmodern}
\usepackage{hyperref, csquotes, textcomp}
\usepackage{listings}
\usepackage{fullpage}
\usepackage[french]{babel}
\usepackage[dvipsnames]{xcolor}
\usepackage{draftwatermark}
\SetWatermarkText{Brouillon}
\SetWatermarkScale{1}
\SetWatermarkColor[gray]{0.92}
\makeatletter
\lstdefinelanguage{lawspec}{%
basicstyle=\ttfamily,
keywordstyle = [1]{\color{BlueViolet}},
keywordstyle = [2]{\color{RedViolet}},
morekeywords = [1]{situation donnee, type, de, donnee, situation,
collection, regle, condition, consequence, existe, pour,
tout, dans, tel, que, optionnelle, defini, comme, source, fixe, par,
assertion, constante, avec, varie, maniere, decroissante, croissante,
choix, parametre, fonction, renvoie, parametres, on, a},
morekeywords = [2]{ou, et, si, alors, entier, booléen, montant, cardinal,
maintenant, an, mois, selon, sous, forme},
otherkeywords = {<, >, =, +, *, --, /, ;, :, .},
morekeywords = [1]{--, ;, :, .},
morekeywords = [2]{=, <, >, +, *, /, -},
% morestring=[b]",
% sensitive=true,%
numbers=left,
firstnumber=last,
numberstyle=\footnotesize\color{gray},
% numbersep=4pt,
% numbers=left,
% columns=[l]fullflexible,
texcl=true,
% mathescape=true,
% xleftmargin=10pt,
% identifierstyle={\ttfamily},
% Here is the range marker stuff
% rangeprefix=(*---\ ,
% includerangemarker=false,
% stringstyle=\rmfamily,
% lineskip=-4pt,
showspaces=false,
showstringspaces=false,
morecomment=[f][\color{gray}][0]{\#},
commentstyle=\color{gray}\itshape,
breaklines=false}
\lstset{language=lawspec}
\makeatother
\title{
Proposition d'un langage de formalisation de textes législatifs :\\
document à l'intention des juristes
}
\author{
Denis Merigoux\\Inria\and
Nicolas Chataing\\Inria -- École Normale Supérieure\and
Liane Huttner\\Université Panthéon-Sorbonne
}
\begin{document}
\maketitle
\section{Guide de lecture}
\paragraph{Programmation littérale} Le texte de la loi est annoté avec des morceaux de code qui traduisent le contenu des articles et alinéa en termes formels. Ces blocs de code sont intercalés dans le texte de loi, remarquables à leur police en chasse fixe et la coloration de certains mots. Un morceau de code annotant une ligne d'un texte de loi doit contenir tout le contenu sémantique de la ligne de texte, et rien d'autre que ce contenu. L'idée est de pouvoir vérifier localement, ligne à ligne, la cohérence entre le code et le texte législatif.
\paragraph{Situations} Une situation correspond à un contexte logique dans un morceau de code. De même que dans un texte législatif, on se met dans une situation particulière dans laquelle les entités et concepts que l'on nomme ont un sens, chaque morceau de code se place dans un contexte bien particulier auquel on donne un nom. Deux morceaux de code partagent le même contexte logique si ils sont introduits par des lignes \lstinline|situation| ayant le même nom. Une ligne \lstinline|situation| précise aussi la source juridique du contenu qui y sera précisé : loi, décret, règlement ou implicite pour un contenu logique non explicité dans la loi mais qui découle du bon sens.
\paragraph{Données} Au sein d'une situation, il est possible de déclarer différentes données (\lstinline|donnee|). Ces données sont les quantités et prédicats que le programme va manipuler. Afin de préciser ces données, chacune d'entre elle est assortie d'un type ou d'une situation qui en décrit le contenu. Un type correspond à des quantités primitives comme les entiers, les booléens (vrai ou faux), les dates, les montants d'argent, etc. Une donnée peut aussi contenir une situation qui elle même contient d'autre données, permettant de donner de la structure. Lorsque rien n'est précisé quant au contenu d'une donnée, c'est qu'il n'y a pas de contenu (ou plutôt le contenu est trivial).
\paragraph{Règles} Le but de l'algorithme est d'exprimer comment calculer une donnée-but en fonction d'un ensemble de données-entrées. Cependant, les textes ne définissent pas de données-but ni de données-entrées ; ils se contente d'exprimer des relations entre les données. Une des relations exprimées par les textes à propos des données est la définition. Les règles (\lstinline|regle|) permettent de définir une donnée en fonction d'autres données de la situation. À l'instar des textes, cette définition peut être conditionnelle, pour cela on utilisera les mots-clés \lstinline|condition| et \lstinline|consequence|.
\paragraph{Assertions} Le deuxième type de relation que les textes expriment sur les données consiste à exiger une condition de cohérence. Les \lstinline|assertion| permettent d'exprimer cette exigence de cohérence ; ces conditions doivent être toujours vraies lorsque l'algorithme s'exécute. Une assertion peut tout aussi bien imposer une condition sur les données en entrée, qu'imposer une propriété que l'algorithme doit vérifier. Par exemple, il est possible d'exiger dans une assertion que telle donnée varie de manière décroissante en fonction d'une autre donnée.
\paragraph{Collections} Parfois, le contenu d'une donnée correspond à une collection de contenus, au nombre indéterminé. Il est possible de déclarer ces \lstinline|collections|, et l'on peut alors accéder aux éléments individuels des collections en utilisant les formule existentielles (\lstinline|existe ... tel que|) ou universelles (\lstinline|pour tout ... on a|).
\paragraph{Choix} Si les \lstinline|situation| permettent de regrouper plusieurs données dans un même contexte, les \lstinline|choix| permettent au contraire d'exprimer une disjonction de cas dans un algorithme. Chaque possibilité du choix peut, à l'instar des données d'une situation, porter un contenu qui peut être un type, une situation ou bien un autre choix. Afin d'examiner dans le code la valeur contenu dans un contenu choix, on utilisera la syntaxe \lstinline|selon ... sous forme|.
\section{Corpus législatif et réglementaire définissant les allocations familiales}
\paragraph{Article L511-1} Les prestations familiales comprennent :\\
1°) la prestation d'accueil du jeune enfant ;\\
2°) les allocations familiales ;\\
3°) le complément familial ;\\
4°) L'allocation de logement régie par les dispositions du livre VIII du code de la construction et de l'habitation ;\\
5°) l'allocation d'éducation de l'enfant handicapé ;\\
6°) l'allocation de soutien familial ;\\
7°) l'allocation de rentrée scolaire ;\\
8°) (Abrogé) ;\\
9°) l'allocation journalière de présence parentale.
\begin{lstlisting}
choix prestation:
-- PrestationAccueilJeuneEnfant
-- AllocationsFamiliales
-- ComplementFamilial
-- AllocationLogement
-- AllocationEducationEnfantHandicape
-- AllocationSoutienFamilial
-- AllocationRentreeScolaire
-- AllocationJournalierePresenceParentale.
situation ContextePrestationsFamiliales source loi :
donnee prestation_courante de choix prestation.
\end{lstlisting}
\paragraph{Article L512-3} Sous réserve des règles particulières à chaque prestation, ouvre droit aux prestations familiales :
\begin{lstlisting}
situation ContextePrestationsFamiliales source loi :
donnee droits_ouverts.
\end{lstlisting}
1°) tout enfant jusqu'à la fin de l'obligation scolaire ;
\begin{lstlisting}
situation EnfantPrestationsFamiliales source loi :
donnee fin_obligation_scolaire de type entier.
situation ContextePrestationsFamiliales source loi :
donnee enfants collection de situation EnfantPrestationsFamiliales ;
regle condition
existe enfant dans enfants tel que
maintenant < enfant.fin_obligation_scolaire
consequence droits_ouverts defini.
\end{lstlisting}
2°) après la fin de l'obligation scolaire, et jusqu'à un âge limite, tout enfant dont la rémunération éventuelle n'excède pas un plafond.
\begin{lstlisting}
situation ContextePrestationsFamiliales source loi :
donnee age_limite_L512_3_2 de type entier ;
donnee plafond_remuneration_L512_3_2 de type montant.
situation EnfantPrestationsFamiliales source loi :
donnee age de type entier ;
donnee remuneration de type montant ;
donnee qualifie_pour_prestation_sauf_age ;
regle condition
maintenant > fin_obligation_scolaire et
remuneration < plafond_remuneration_L512_3_2
consequence qualifie_pour_prestation_sauf_age defini ;
donnee enfant_qualifie_pour_prestation ;
regle condition
qualifie_pour_prestation_sauf_age et
age < age_limite_L512_3_2
consequence qualifie_pour_prestation defini.
situation ContextePrestationsFamiliales source loi :
regle condition
existe enfant dans enfants tel que
enfant.qualifie_pour_prestation
consequence droits_ouverts defini.
\end{lstlisting}
Toutefois, pour l'attribution du complément familial et de l'allocation de logement mentionnés aux 3° et 4° de l'article L. 511-1, l'âge limite peut être différent de celui mentionné au 2° du présent article.
\begin{lstlisting}
situation ContextePrestationsFamiliales source loi :
donnee age_limite_L512_3_2_alternatif de type entier ;
regle optionnelle condition
prestation_courante = ComplementFamilial ou
prestation_courante = AllocationLogement
consequence
age_limite_L512_3_2 defini comme age_limite_L512_3_2_alternatif.
\end{lstlisting}
\paragraph{Article L521-1} Les allocations familiales sont dues à partir du deuxième enfant à charge.
\begin{lstlisting}
situation AllocationsFamiliales source loi:
donnee contexte de situation ContextePrestationsFamiliales ;
regle contexte.prestation_courante
defini comme AllocationsFamiliales ;
donnee allocations_familiales_dues ;
donnee nombre_enfants_a_charge : entier.
regle nombre_enfants_a_charge defini comme cardinal(contexte.enfants) ;
regle condition
nombre_enfants_a_charge >= 2
consequence allocations_familiales_dues defini.
\end{lstlisting}
Une allocation forfaitaire par enfant d'un montant fixé par décret est versée pendant un an à la personne ou au ménage qui assume la charge d'un nombre minimum d'enfants également fixé par décret lorsque l'un ou plusieurs des enfants qui ouvraient droit aux allocations familiales atteignent l'âge limite mentionné au 2° de l'article L. 512-3. Cette allocation est versée à la condition que le ou les enfants répondent aux conditions autres que celles de l'âge pour l'ouverture du droit aux allocations familiales.
\begin{lstlisting}
situation AllocationFamiliales source loi :
donnee allocation_forfaitaire_L521_1 de type montant ;
assertion allocation_forfaitaire_L521_1 fixe par decret ;
donnee nombre_minimum_enfants_L521_1 de type entier ;
assertion nombre_minimum_enfants_L521_1 fixe par decret.
choix entite_en_charge :
-- FamilleMonoparentale de situation Personne
-- Couple de situation Menage.
situation AllocationFamiliales source loi :
donnee entite_en_charge_des_enfants de choix entite_en_charge ;
constante duree_allocation_familiale de type duree defini comme 1 an.
donnee propriete allocation_forfaitaire_L521_1_versee ;
regle conditon
nombre_enfants_a_charge > nombre_minimum_enfants_L521_1 et
(existe enfant dans contexte.enfants tel que
enfant.age = age_limite_L512_3_2 et
enfant.qualifie_pour_prestation_sauf_age)
consequence allocation_forfaitaire_L521_1_versee defini.
\end{lstlisting}
Le montant des allocations mentionnées aux deux premiers alinéas du présent article, ainsi que celui des majorations mentionnées à l'article L. 521-3 varient en fonction des ressources du ménage ou de la personne qui a la charge des enfants, selon un barème défini par décret.
\begin{lstlisting}
situation Personne source implicite :
donnee ressources de type montant.
situation Menage source implicite :
donnee ressources de type montant ;
donnee parent1 de situation Personne ;
donnee parent2 de situation Personne ;
regle ressources defini comme
parent1.ressources + parent2.ressources.
situation AllocationFamiliales source loi :
donnee ressources_entite_en_charge de type montant.
regle ressources_entite_en_charge defini comme
selon entite_en_charge_enfants sous forme
-- FamilleMonoparentale de parent : parent.ressources
-- Couple de menage : menage.ressources ;
donnee montant_allocations_familiales de type montant ;
assertion
montant_allocations_familiales fixe par decret et
montant_allocations_familiales varie avec ressources_entite_en_charge ;
assertion
allocation_forfaitaire_L521_1 fixe par decret et
allocation_forfaitaire_L521_1 varie avec ressources_entite_en_charge ;
donnee majorations_512_3 de type montant ;
assertion
majorations_512_3 fixe par decret et
majorations_512_3 varie avec ressources_entite_en_charge.
\end{lstlisting}
Le montant des allocations familiales varie en fonction du nombre d'enfants a charge.
\begin{lstlisting}
situation AllocationFamiliales source loi :
assertion
montant_allocations_familiales varie avec de nombre_enfants_a_charge.
\end{lstlisting}
Les niveaux des plafonds de ressources, qui varient en fonction du nombre d'enfants à charge, sont révisés conformément à l'évolution annuelle de l'indice des prix à la consommation, hors tabac.
\begin{lstlisting}
situation AllocationFamiliales source loi :
donnee plafonds_ressources_allocations_familiales
collection de type montant ;
assertion
pour tout plafond dans plafonds_ressources_allocations_familiales on a
plafond varie avec nombre_enfants_a_charge.
# TODO: comment parler de l'évolution?
\end{lstlisting}
Un complément dégressif est versé lorsque les ressources du bénéficiaire dépassent l'un des plafonds, dans la limite de montants définis par décret. Les modalités de calcul de ces montants et celles du complément dégressif sont définies par décret.
\begin{lstlisting}
situation AllocationFamiliales source loi :
donnee complement_degressif_allocations_familiales de type montant ;
assertion complement_degressif_allocations_familiales varie avec
nombre_enfants_a_charge de maniere decroissante ;
assertion
complement_degressif_allocations_familiales fixe par decret.
\end{lstlisting}
\paragraph{Article L521-2} Les allocations sont versées à la personne qui assume, dans quelques conditions que ce soit, la charge effective et permanente de l'enfant.
\begin{lstlisting}
situation RecipendaireDivise source implicite :
donnee recipiendaire1 de situation Personne ;
donnee recipiendaire2 de situation Personne ;
situation EnfantAllocationsFamiliales source loi :
donnee contexte de situation EnfantPrestationsFamiliales ;
donnee entite_en_charge_de_l_enfant de choix entite_en_charge.
situation AllocationFamiliales source loi :
donnee enfants collection de situation EnfantAllocationsFamiliales ;
regle cardinal(enfants) defini comme cardinal(contexte.enfants) ;
regle pour tout enfant_contexte, enfants
dans enfants.contexte, enfants on a
enfant.contexte defini comme enfant_contexte ;
regle pour tout enfant dans enfants on a
enfant.entite_en_charge_de_l_enfant defini comme
entite_en_charge_des_enfants
choix recipiendaire:
-- Complet de choix entite_en_charge
-- Divise de situation RecipendaireDivise.
situation EnfantAllocationsFamiliales source loi :
donnee recipiendaire_allocations de type recipiendaire ;
regle recipiendaire_allocations defini comme
Complet de entite_en_charge_de_l_enfant.
\end{lstlisting}
En cas de résidence alternée de l'enfant au domicile de chacun des parents telle que prévue à l'article 373-2-9 du code civil, mise en oeuvre de manière effective, les parents désignent l'allocataire. Cependant, la charge de l'enfant pour le calcul des allocations familiales est partagée par moitié entre les deux parents soit sur demande conjointe des parents, soit si les parents sont en désaccord sur la désignation de l'allocataire. Un décret en Conseil d'Etat fixe les conditions d'application du présent alinéa.
\begin{lstlisting}
situation EnfantAllocationsFamiliales source loi :
donnee garde_alternee ;
# on ne formalise pas l'article 373-2-9 pour l'instant
donnee parent1_garde_alternee de situation Personne ;
donnee parent2_garde_alternee de situation Personne ;
fonction est_en_charge parametres
-- parent de situation Personne
renvoie booleen:
selon entite_en_charge_de_l_enfant sous forme
-- FamilleMonoparentale de parent' : parent = parent'
-- Couple de menage :
menage.parent1 = parent ou menage.parent2 = parent ;
assertion condition garde_alternee consequence
est_en_charge de parent1_garde_alternee ou
est_en_charge de parent2_garde_alternee ;
donnee parent_recipiendaire_garde_alternee de situation Personne ;
regle condition garde_alternee consequence
recipiendaire_allocations defini comme
Complet de parent_recipiendaire_garde_alternee ;
donnee desaccord_designation_allocataire_garde_alternee ;
donnee demande_conjointe_partage_charge_garde_alternee ;
donnee recipiendaire_divise_garde_alternee
de situation RecipiendaireDivise ;
regle condition garde_alternee et
(desaccord_designation_allocataire_garde_alternee ou
demande_conjointe_partage_charge_garde_alternee)
consequence
-- recipiendaire_divise_garde_alternee.parent1 defini comme
parent1_garde_alternee
-- recipiendaire_divise_garde_alternee.parent2 defini comme
parent2_garde_alternee
-- recipiendaire_allocations defini comme
Divise de recipiendaire_divise_garde_alternee ;
assertion selon recipiendaire_allocations sous forme
-- Complet de (FamilleMonoparentale de personne) :
est_en_charge de personne;
-- Complet de (Couple de couple) :
Couple de couple = entite_en_charge_enfants
-- Divise : vrai.
\end{lstlisting}
Lorsque la personne qui assume la charge effective et permanente de l'enfant ne remplit pas les conditions prévues au titre I du présent livre pour l'ouverture du droit aux allocations familiales, ce droit s'ouvre du chef du père ou, à défaut, du chef de la mère.
\begin{lstlisting}
situation EnfantAllocationsFamiliales source loi :
donnee entite_en_charge_des_enfants_remplit_les_conditions_du_titre_I.
assertion
entite_en_charge_des_enfants_remplit_les_conditions_du_titre_I.
# on ne formalise pas pour l'instant, c'est un placeholder.
\end{lstlisting}
Lorsqu'un enfant est confié au service d'aide sociale à l'enfance, les allocations familiales continuent d'être évaluées en tenant compte à la fois des enfants présents au foyer et du ou des enfants confiés au service de l'aide sociale à l'enfance. La part des allocations familiales dues à la famille pour cet enfant est versée à ce service. Toutefois, le juge peut décider, d'office ou sur saisine du président du conseil général, à la suite d'une mesure prise en application des articles 375-3 et 375-5 du code civil ou des articles 15,16,16 bis et 28 de l'ordonnance n° 45-174 du 2 février 1945 relative à l'enfance délinquante, de maintenir le versement des allocations à la famille, lorsque celle-ci participe à la prise en charge morale ou matérielle de l'enfant ou en vue de faciliter le retour de l'enfant dans son foyer.
\begin{lstlisting}
situation EnfantAllocationsFamiliales source loi :
donnee enfant_confie_au_service_sociaux.
donnee service_social : Personne.
regle optionnelle condition enfant_confie_au_service_sociaux
consequence recipiendaire_allocations defini comme
Complet de (FamilleMonoparentale de service_social)
\end{lstlisting}
Un décret en Conseil d'Etat fixe les conditions d'application du présent article, notamment dans les cas énumérés ci-dessous :
a) retrait total de l'autorité parentale des parents ou de l'un d'eux ;
b) indignité des parents ou de l'un d'eux ;
c) divorce, séparation de corps ou de fait des parents ;
d) enfants confiés à un service public, à une institution privée, à un particulier.
\begin{lstlisting}
choix couple_ou_partie :
-- DeuxParents
-- Parent1
-- Parent2.
situation EnfantAllocationsFamiliales source loi :
donnee retrait_autorite_parentale de choix couple_ou_partie ;
donnee indignite_parents de choix couple_ou_partie ;
fonction couple_ou_partie_valide parametres
-- partie de choix couple_ou_partie
renvoie booleen :
selon entite_en_charge_de_l_enfant sous forme
-- FamilleMonoparentale de parent : partie = Parent1
-- Couple de couple : vrai ;
asserttion couple_ou_partie_valide retrait_autorite_parentale et
couple_ou_partie_valide indignite_parents ;
donnee propriete divorce_parents ;
donnee enfant_confie_service_public_institution ;
assertion recipiendaire_allocations fixe par decret ;
assertion recipiendaire_allocations varie avec
retrait_autorite_parentale ;
assertion recipiendaire_allocations varie avec indignite_parents ;
assertion recipiendaire_allocations varie avec divorce_parents ;
assertion recipiendaire_allocations varie avec
enfant_confie_service_public_institution.
\end{lstlisting}
\paragraph{Article L521-3} Chacun des enfants à charge, à l'exception du plus âgé, ouvre droit à partir d'un âge minimum à une majoration des allocations familiales.
\begin{lstlisting}
situation AllocationFamiliales source loi :
donnee age_minimum_majorations_512_3 de type entier ;
donnee droits_ouverts_majorations_allocations_familiales ;
donnee enfant_plus_age de situation EnfantAllocationsFamiliales ;
regle enfant_plus_age defini comme
maximum_collection(contexte.enfants, age) ;
regle condition existe enfant dans enfants tel que
enfant.age > age_minimum_majorations_512_3 et
non (enfant = enfant_plus_age)
consequence
droits_ouverts_majorations_allocations_familiales.
\end{lstlisting}
Toutefois, les personnes ayant un nombre déterminé d'enfants à charge bénéficient de ladite majoration pour chaque enfant à charge à partir de l'âge mentionné au premier alinéa.
\begin{lstlisting}
situation AllocationFamiliales source loi :
donnee nombre_enfants_a_charge_L521_3 de type entier.
regle condition
nombre_enfants_a_charge = nombre_enfants_a_charge_L521_3 et
existe enfant dans enfants tel que
enfant.age > age_minimum_majorations_512_3
consequence
droits_ouverts_majorations_allocations_familiales.
\end{lstlisting}
\end{document}