




版权说明:本文档由用户提供并上传,收益归属内容提供方,若内容存在侵权,请进行举报或认领
文档简介
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年新型分子筛系列产品项目合作计划书
- 2025年玻璃、陶瓷制品生产专用设备合作协议书
- 2025年邮政专用机械及器材项目建议书
- 2025年高纯度丙烯酰胺及聚丙烯酰胺项目建议书
- 学习动力与教育环境的互动关系
- 教育创新论坛国际在线教育平台的挑战与机遇
- 教育国际合作打破教育壁垒的实践研究
- 肺结节中医课件
- 护理核心制度考试试卷(附答案)
- 汽车之夜活动方案
- DB33∕642-2019 热电联产能效、能耗限额及计算方法
- 考试录用公务员笔试监考工作培训
- GM∕T 0036-2014 采用非接触卡的门禁系统密码应用指南
- 钱江杯优质工程检查表
- 内蒙古高中毕业生学籍表毕业生登记表学年评语表成绩单身体健康检查表完整版高中档案文件
- NMRV减速机说明
- 小升初火车过桥问题
- 动叶可调式轴流风机动叶调节原理图
评论
0/150
提交评论