版权说明:本文档由用户提供并上传,收益归属内容提供方,若内容存在侵权,请进行举报或认领
文档简介
1、Rcriture pour la programmation et la preuve,Claude Kirchner Pierre-Etienne Moreau,Application XML,Document XML,XML permet de dcrire des documents structurs Paul Mark Jurgen Julien Pierre On peut voir un document XML comme un arbre,Transformation de documents XML,On a envie de pouvoir manipuler ces d
2、onnes pour y rechercher de linformation pour gnrer de nouveaux documents (HTML, LaTeX, PDF, XML, etc.) Quels sont les outils permettant de le faire XSLT / XPath Xquery Xduce / Cduce DOM Peu permettent de manipuler un document XML en Java Les manipulations se font souvent en utilisant DOM directement
3、,Exemple,On veut savoir sil existe un noeud de la forme Julien Paul Mark Jurgen Julien Pierre ,Filtrage,Il faut savoir si un pattern XML filtre vers un noeud de document XML On aimerait pouvoir crire %match(t) Julien - / Noeud trouv Ou plus gnralement : X - ,Modle de donne (simplifi),ElementNode(nam
4、e:str, attrList:TNodeList, childList:TNodeList) - TNode AttributeNode(name:str, value:str) - TNode TextNode(data:str) - TNode conc(TNode*) - TNodeList,XML vs. Term,Un document XML peut se voir comme un arbre est reprsent par : ElementNode(A, conc(AttributeNode(a, at1), conc(ElementNode(B,conc(),conc
5、() ),Pattern XML,On veut pouvoir crire un pattern de la forme X qui sera encod par : ElementNode(A, conc(AttributeNode(a, at1), conc(X) ),Questions,A-t-on : X ? X ? Quel est le type de X ? TNode ? TNodeList ? On voudrait pouvoir crire X* Quelles sont les solutions ?,Questions,En fonction du parseur,
6、 peut tre reconnu comme A-t-on : X ? X* ? Comment est encod ? ElementNode(A, conc(AttributeNode(a, at1), conc( TextNode(), ElementNode(B,conc(),conc(), TextNode() ) Est-ce que cela filtre ?,Notation explicite,(_*,X,_*) qui correspond : conc(_*,X,_*) A-t-on (_*,X,_*) ? Oui, il y a 3 solutions,Notatio
7、n implicite,(_*,X,_*) qui correspond : X qui correspond galement X A-t-on X ? Oui, il y a 3 solutions,Attributs,Les attributs sont reprsents par une liste de couples (nom,valeur) Il existe galement des notations implicites et explicites Ainsi : correspond qui correspond ,Questions,A-t-on : ? ? Pourq
8、uoi ? car ? A-t-on : ? ? Non, car : (_*, a=at1, _*, b=at2, _*) ! (b=at2, a=at1) Il faudrait du filtrage AC avec lment neutre!,Attributs dans Tom,On considre un ordre sur les noms dattributs et les formes canoniques o les attributs sont tris Ainsi, est reprsent par ElementNode(A, conc(AttributeNode(a
9、, at1), AttributeNode(b, at2), conc() De mme, pour les motifs,Utilisation dans Tom,Node sort(Node subject) %match(subject) (X1*,p1,X2*,p2,X3*) - if(compare(p1,p2) 0) return sort(xml( X1* p2 X2* p1 X3* ); return subject; ,Comparaison dattributs,int compare(Node t1, Node t2) %match(t1, t2) n1 , n2 - r
10、eturn pareTo(a2); return 0; ,Ancrage formel,Mapping,Problmatique,Comment faciliter lutilisation du filtrage dans les programmes existants ? en permettant un mlange des syntaxes en permettant de filtrer vers des structures du langage hte Nous avons donc besoin de filtrer modulo des vues,Solution adop
11、te,Tom permet de voir les objets en mmoire comme des termes algbrique Il faut pour cela dfinir un ancrage formel permettant de savoir si un terme commence par un symbole donn daccder un sous terme donn,Plus formellement,On considre les ensembles : N, la reprsentation des entiers naturels B, la reprs
12、entation des boolens F, la reprsentation des symboles T(F), la reprsentation des termes clos X, la reprsentation des variables,Contraintes respecter,t1,t2T(F), eq(t1,t2) = t1=t2 fF, tT(F), is_fsym(t,f) = Symb(t)=f fF, i1.ar(f), tT(F) subtermf(t,i) = t|i,Structure de donnes,struct term int symb; stru
13、ct term *subterm; On reprsente les symboles par des entiers (zero,3), (suc,5), (plus,7), ,Mapping de Nat vers une structure C,%typeterm Nat implement equals(t1,t2) %op Nat zero is_fsym(t) %op Nat suc(p:Nat) is_fsym(t) get_slot(p,t) , struct term* term_equals(t1,t2) t!=null class B extends A int b; %
14、typeterm A implement A equals(t1,t2) t1.equals(t2) %typeterm B implement B equals(t1,t2) t1.equals(t2) ,Mapping objet,%op A A(a:int) is_fsym(t) t instanceof A get_slot(a,t) t.a %op A B(a:int,b:int) is_fsym(t) t instanceof B get_slot(a,t) t.a get_slot(b,t) t.b Aa=x new A(3) Bb=x new B(2,3) Aa=x new B
15、(2,3),Demo,Questions,Doit-on crire des mappings ? Que fait %vas au juste ?,Outils autour de Tom,Aterm, SDF, ApiGen, Vas,Bibliothque ATerm,Aterm AFun ATermAppl ATermList ATermInt ATermReal ATermPlaceholder ATermBlob ATermFactory,ATerms,Bibliothque ATerm,Aterm AFun ATermAppl ATermList ATermInt ATermRe
16、al ATermPlaceholder ATermBlob ATermFactory,getAnnotation setAnnotation toString etc.,Bibliothque ATerm,Aterm AFun ATermAppl ATermList ATermInt ATermReal ATermPlaceholder ATermBlob ATermFactory,getName getArity,Bibliothque ATerm,Aterm AFun ATermAppl ATermList ATermInt ATermReal ATermPlaceholder ATerm
17、Blob ATermFactory,getAFun getArgument setArgument etc.,Bibliothque ATerm,Aterm AFun ATermAppl ATermList ATermInt ATermReal ATermPlaceholder ATermBlob ATermFactory,getFirst getNext elementAt insert append concat etc.,Bibliothque ATerm,Aterm AFun ATermAppl ATermList ATermInt ATermReal ATermPlaceholder
18、 ATermBlob ATermFactory,makeAFun makeAppl parse readFromFile etc.,Utilisation des ATerms,Aterm t1 = factory.parse(a) Aterm t2 = factory.parse(f(a,b) t2.getArgument(1) = t1 ? true Aterm t3 = t2.setArgument(t1,2) t3 = f(a,a) Aterm t4 = factory.parse(f(a,f(b) f na pas de signature particulire Les Aterm
19、s permettent de construire des termes, mais il ny a pas de scurit (signature, types),ApiGen / Vas,A partir dune signature multi-sorte Gnre des classes, reposant sur les Aterms, permettant de reprsenter les termes partage maximal typage fort des termes tout terme typ est un ATerm,Exemple,Module Expre
20、ssions true - Bool false - Bool eq(lhs:Expr, rhs:Expr) - Bool id(value:str) - Expr nat(value:int) - Expr add(lhs:Expr, rhs:Expr) - Expr mul(lhs:Expr, rhs:Expr) - Expr,Classes gnres,Classes gnres,Stratgies,Programmation par rcriture,Avantages le filtrage est un mcanisme expressif les rgles expriment
21、des transformations lmentaires Limitations les systmes de rgles sont souvent non-terminant et/ou non confluent en gnral, on ne veut pas appliquer toutes les rgles en mme temps,Exemple de systme non terminant,And(Or(x,y),z) Or(And(x,z),And(y,z) And(z,Or(x,y) Or(And(z,x),And(z,y) Or(And(x,y),z) And(Or
22、(x,z),Or(y,z) Or(z,And(x,y) And(Or(z,x),Or(z,y) Not(Not(x) x Not(And(x,y) Or(Not(x),Not(y) Not(Or(x,y) And(Not(x),Not(y),Codage du contrle dans les rgles,Solution classique introduire un nouvel oprateur f pour restreindre lensemble de rgles permettant de normaliser l r devient f(l) r on normalise un
23、 terme f(t) loprateur f permet de contrler les rgles appliquer,Encodage du contrle,f(And(x,y) and(x,y) f(Not(x) not(x) f(Or(x,y) Or(f(x),f(y) and(Or(x,y),z) Or(and(x,z),and(y,z) and(z,Or(x,y) Or(and(z,x),and(z,y) and(x,y) And(x,y) not(Not(x) x not(And(x,y) Or(not(x),not(y) not(Or(x,y) and(not(x),not
24、(y) not(x) Not(x),Consquences,Il faut dfinir la congruence explicitement, pour chaque rgle et chaque constructeur Il ny a plus de sparation entre transformation et contrle cela rend la comprhension plus difficile les rgles sont moins rutilisables,Ce quon voudrait,pouvoir contrle lapplication des rgl
25、es pouvoir spcifier simplement le traverse dune terme (I.e. appliquer une rgles dans les sous-termes) tout en sparant rgle et contrle,Solution,Utiliser des stratgies Combiner des transformations lmentaires Exemples disjunctive normal form dnf = innermost(DAOL + DAOR + DN +) DAOL : And(Or(x,y),z) Or(
26、And(x,z),And(y,z) DAOR : And(z,Or(x,y) Or(And(z,x),And(z,y) DN : Not(Not(x) x conjunctive normal form cnf = innermost(DOAL + DOAR + DN +),Autres stratgies de traverse,simplify = bottomup(repeat(R1 + ) simplify = topdown(repeat(R1 + ) Slide 14,Stratgies en Tom,Constructeurs lmentaires,Identity Fail N
27、ot Sequence Choice All One Some IfThenElse Omega mu,Dfinition de stratgies,%op VisitableVisitor Try(s1:VisitableVisitor) make(v) Choice(v,Identity) %op VisitableVisitor Repeat(s1:VisitableVisitor) make(v) mu(MuVar(x),Choice(Sequence(v,MuVar(x),Identity() %op VisitableVisitor TopDown(s1:VisitableVisi
28、tor) make(v) mu(MuVar(x),Sequence(v,All(MuVar(x) %op VisitableVisitor OnceBottomUp(s1:VisitableVisitor) make(v) mu(MuVar(x),Choice(One(MuVar(x),v) %op VisitableVisitor Innermost(s1:VisitableVisitor) make(v) mu(MuVar(x),Sequence(All(MuVar(x), Try(Sequence(v,MuVar(x) ,Stratgie lmentaire en Tom,class R
29、ewriteSystem extends strategy.term.termVisitableFwd public RewriteSystem() super(Fail(); public Term visit_Term(Term arg) throws VisitFailure %match(Term arg) a() - return b(); b() - return c(); g(c(),c() - return c(); throw new VisitFailure(); ,Utilisations,VisitableVisitor rule = new RewriteSystem
30、(); Term subject = f(g(g(a,b),g(a,a); OnceBottomUp(rule).visit(subject); Innermost(rule).visit(subject); Repeat(OnceBottomUp(rule).visit(subject);,(mode paranoaque),VisitableVisitor rule = new RewriteSystem(); Term subject = f(g(g(a,b),g(a,a); VisitableVisitor onceBottomUp = mu(MuVar(x),Choice(One(M
31、uVar(x),rule); onceBottomUp.visit(subject); VisitableVisitor innermostSlow = mu(MuVar(y),Choice(Sequence(onceBottomUp,MuVar(y),Identity(); innermostSlow.visit(subject); VisitableVisitor innermost = mu(MuVar(x),Sequence(All(MuVar(x),Choice(Sequence(rule,MuVar(x),Identity); innermost.visit(subject);,Questions,Comment calculer des ensembles de rsultats Exemples f(g(g(a,b),g(a,b) trouver les x tels que g(x,b) filtre un so
温馨提示
- 1. 本站所有资源如无特殊说明,都需要本地电脑安装OFFICE2007和PDF阅读器。图纸软件为CAD,CAXA,PROE,UG,SolidWorks等.压缩文件请下载最新的WinRAR软件解压。
- 2. 本站的文档不包含任何第三方提供的附件图纸等,如果需要附件,请联系上传者。文件的所有权益归上传用户所有。
- 3. 本站RAR压缩包中若带图纸,网页内容里面会有图纸预览,若没有图纸预览就没有图纸。
- 4. 未经权益所有人同意不得将文件中的内容挪作商业或盈利用途。
- 5. 人人文库网仅提供信息存储空间,仅对用户上传内容的表现方式做保护处理,对用户上传分享的文档内容本身不做任何修改或编辑,并不能对任何下载内容负责。
- 6. 下载文件中如有侵权或不适当内容,请与我们联系,我们立即纠正。
- 7. 本站不保证下载资源的准确性、安全性和完整性, 同时也不承担用户因使用这些下载资源对自己和他人造成任何形式的伤害或损失。
最新文档
- 2025-2026学年中华孝道朗诵说课稿
- 2026年成都市金牛区公务员人员招聘考试备考题库及答案详解
- 2025-2026学年大班滚进球门说课稿
- 2026武汉生物工程学院博士教师招聘笔试参考题库及答案解析
- 2026年佳木斯市东风区公务员人员招聘笔试模拟试题及答案详解
- 2025-2026学年初一思品说课稿
- 高中生物学人教版(2019)必修二 第4章 基因的表达 单元检测试卷(含答案)
- 2025-2026学年大象滚球绘画说课稿
- 2026年庆阳市西峰区公务员人员招聘笔试备考题库及答案详解
- 2025-2026学年大班换牙说课稿科学
- 2026年黄山市公共交通有限公司招聘3名笔试备考题库及答案详解
- 2026人教版九年级物理(全一册)知识点总结
- 《高三物理竞赛暑假系统复习课件》
- 国家电网公文写作与申论专项突破涵盖通知、通报、纪要、调研报告等常考文种含15篇批注版范文
- 《中华人民共和国生态环境法典》深度培训
- 2026年证券公司营业部总经理竞聘管理能力面试问题含答案
- T∕CNLIC 0218-2025 乳源酵母菌、乳酸菌发酵型含乳饮料 奶啤
- 上海市奉贤区2025-2026学年高三上学期一模语文试卷(含答案)
- 中国心血管健康与疾病报告(2024年)要点解读课件
- 生命教育主体班会课件
- 《旅游管理专业介绍》课件
评论
0/150
提交评论