中国科学院软件研究所 计算机科学国家重点实验室 张文辉

Slides:



Advertisements
Similar presentations
真题解析 2013 湖南公务员面试专项辅导 华图面试研究员 张鑫 cn.
Advertisements

While 迴圈 - 不知重複執行次數
年鉴实务培训 北京年鉴社 2014·09.
名人介紹 名字:巴拉克.歐巴馬.
《C语言程序设计》复习
親愛的老師您好 感謝您選用本書作為授課教材,博碩文化準備本書精選簡報檔,特別摘錄重點提供給您授課專用。 說明: 博碩文化:
迴圈 迴圈基本觀念 while迴圈 do 迴圈 for迴圈 巢狀迴圈 迴圈設計注意事項 其他控制指令 迴圈與選擇的組合.
计算学科的基本问题 本章首先介绍一个对问题进行抽象的典型实例——哥尼斯堡七桥问题。然后,通过“梵天塔”问题和“停机问题”分别介绍学科中的可计算问题和不可计算问题。从“梵天塔”问题再引出算法复杂性中的难解性问题、P类问题和NP类问题,证比求易算法,P=NP是否成立的问题。
“八皇后”问题 崔萌萌 吕金华.
安 全 維 護 臺 東 林 區 管 理 處 消費安全 詐騙防範宣導 健康生活 毒家新聞 杜絕不明匯款及金融轉帳操作
第一章 C语言概述 计算机公共教学部.
计算机与程序.
如何开好通表会 荔湾区教育局第二期学生团干培训 2009年9月 1.
計畫主持人:謝麗華、諶亦聰、李侃諭 協同主持人:國語、數學、英語、社會、 自然領域輔導團 計畫執行:專業發展組北投國小
跳楼价 亏本大甩卖 清仓处理 买一送一 5折酬宾. 跳楼价 亏本大甩卖 清仓处理 买一送一 5折酬宾.
11 物流仿真技术 11.1物流系统仿真 11.2 物流仿真方法 知识归纳 复习题.
仓颉造字 相传仓颉在黄帝手下当官。那时,当官的可并不显威风,和平常人一样,只是分工不同。黄帝分派他专门管理圈里牲口的数目、屯里食物的多少。仓颉这人挺聪明,做事又尽力尽心,很快熟悉了所管的牲口和食物,心里都有了谱,难得出差错。可慢慢的,牲口、食物的储藏在逐渐增加、变化,光凭脑袋记不住了。当时又没有文字,更没有纸和笔。怎么办呢?仓颉犯难了。
補充: Input from a text file
[聚會時,請將傳呼機和手提電話關掉,多謝合作]
他們,與眾不同…….
[聚會時,請將傳呼機和手提電話關掉,多謝合作]
C++程序设计 王希 图书馆三楼办公室.
第三章 控制结构.
機車第六篇 事故預防 單元二 行駛中注意事項.
循环结构又称为重复结构:用来处理需要重复处理的问题,它是程序中一种很重要的结构。
Class 2 流程控制-選擇敘述與迴圈.
C++Primer 3rd edition 中文版 Chap 5
Chap 10 函数与程序结构 10.1 函数的组织 10.2 递归函数 10.3 宏定义 10.4 编译预处理.
If … else 選擇結構 P27.
第一章 C語言概論 本章投影片僅供本書上課教師使用,非經同意請勿拷貝或轉載.
程式撰寫流程.
中国科学院软件研究所 计算机科学国家重点实验室 张文辉
Introduction to the C Programming Language
1. 說明一個一維整數陣列passwd,下標範圍0至49 2. 在屏幕顯示 "Enter password"
C语言 程序设计基础与试验 刘新国、2012年秋.
第二章 程序的灵魂--算法.
本章中將會更詳細地考慮有關重複的概念,並且會 介紹for和do…while等兩種用來控制重複的敘述 式。 也將會介紹switch多重選擇敘述式。 我們會討論直接和迅速離開某種控制敘述式的 break敘述式,以及用來跳過重複敘述式本體剩餘 部份的continue敘述式。 本章會討論用來組合控制條件的邏輯運算子,最後.
模型验证器VERDS Wenhui Zhang 31 MAY 2011.
C++语言程序设计 第二章 C++简单程序设计.
計數式重複敘述 for 迴圈 P
第1章 概述 本章要点: C语言程序结构和特点 C语言程序的基本符号与关键字 C语言程序的编辑及运行 学习方法建议:
C语言大学实用教程 第5章 函数与程序结构 西南财经大学经济信息工程学院 刘家芬
二元一次聯立方程式 代入消去法 加減消去法 自我評量.
程式結構&語法.
判別下列何者是 x 的多項式。以「○」表示是x的多項式,「×」表示不是 x的多項式 :
4 條件選擇 4.1 程式基本結構 循序式結構 選擇式結構 重複式結構 4-3
第一章 程序设计和C语言 主讲人:高晓娟 计算机学院.
C语言程序示例: 1.输入10个数,按从小到大的顺序排序。 2.汉诺塔问题。.
C++语言程序设计 C++语言程序设计 第三章 控制语句 第十一组 C++语言程序设计.
C 语言程序设计 程序的循环结构 电大崇信县工作站 梁海亮.
第2章 算法与C语言程序 程序 (1)数据的描述:数据的类型和组织形式(数据结构) (2)操作的描述:操作步骤(算法) 沃思指出:
函式庫補充資料.
Chap 5 函数 5.1 计算圆柱体积 5.2 使用函数编写程序 5.3 变量与函数.
7.1 C程序的结构 7.2 作用域和作用域规则 7.3 存储属性和生存期 7.4 变量的初始化
第一章 C语言概述 教师:周芸.
第2章 认识C语言 教学要点 2. 1 项目二C语言程序识读 2 .2 项目三班级成绩排名 2 .3 知识链接 返回.
資料結構與C++程式設計進階 遞迴(Recursion) 講師:林業峻 CSIE, NTU 6/ 17, 2010.
第二章 类型、对象、运算符和表达式.
本节内容 函数嵌套调用的内存布局 视频提供:昆山爱达人信息技术有限公司 官网地址: 联系QQ: QQ交流群 : 联系电话:
程序设计基础.
#include <iostream.h>
第二章 Java基本语法 讲师:复凡.
第五章 逻辑运算和判断选取控制 §5.1 关系运算符和关系表达式
第七章  数 组.
第1章 数据结构基础概论 本章主要介绍以下内容 数据结构研究的主要内容 数据结构中涉及的基本概念 算法的概念、描述方法以及评价标准.
第一次上機考參考答案 僅供參考,同學可自行再想更好的方法..
C语言基本语句 判断循环.
第三章 流程控制 程序的运行流程 选择结构语句 循环结构语句 主讲:李祥 时间:2015年10月.
函式庫補充資料 1.
隨機函數.
Presentation transcript:

中国科学院软件研究所 计算机科学国家重点实验室 张文辉 http://lcs.ios.ac.cn/~zwh/ 模型检测 – 例子 中国科学院软件研究所 计算机科学国家重点实验室 张文辉 http://lcs.ios.ac.cn/~zwh/

程序正确的重要性 应用广泛 软件错误的可能后果 航空 航天 金融 设备的控制 日常生活 火箭 Ariane 5 Explosion (1997) 火星气候轨道器 NASA Mars Climate Orbiter (1999)

程序正确性方法 测试 形式验证 黑盒测试 白盒测试 推理验证 模型检测 可执行代码 程序代码 程序代码或其抽象模型 程序运行环境模型 规则 算法

例子: ISR ./isr INFO: system is now active N: 2 RESULT: 1 N: 10 #include <stdio.h> /**************************************************/ int in(); int isr(int x,int k); int isk(int n,int k); int main() { int n=0; int m=0; int k=1; printf("INFO: system is now active\n"); while (1) { n=in(); m=isr(n,k); k=isk(n,k); printf("RESULT: %i\n\n",m); } int isr(int x,int k) int y1=0; int y2=0; int y3=0; y1=0; y2=1; y3=1; if (x==2||(x>2&&k==20)) x=x-1; while (y3<=x) { y1=y1+1; y2=y2+2; y3=y3+y2; return y1; int isk(int n,int k) if (k!=20) { if (k!=n) k=21; else if (k==19) k=0; else k=k+2; } else { k=21; return k; int in() char c=0; int k=0; k=0; putc('N',stdout); putc(':',stdout); putc(9,stdout); c=getc(stdin); if (c=='\n') { printf("INFO: the input must be 1 or 2 digits\n\n"); continue; if (c<'0'||c>'9') { if (c=='\n') break; k=c-'0'; if (c=='\n') { return k; } if (k<2) k=k*10+(c-'0'); else if (k==2&&c=='0') k=20; else { printf("INFO: the input number must be in {0,...,20}\n\n "); if (c!='\n') { ./isr INFO: system is now active N: 2 RESULT: 1   N: 10 RESULT: 3 N: 20 RESULT: 4 N: 30 INFO: the input number must be in {0,...,20} N: 5 RESULT: 2 N:

例子: ISR 输入为0和20之间的整数时, 输出为其平方根的整数部分。 对ISR的要求: 输入为0和20之间的整数时, #include <stdio.h> /**************************************************/ int in(); int isr(int x,int k); int isk(int n,int k); int main() { int n=0; int m=0; int k=1; printf("INFO: system is now active\n"); while (1) { n=in(); m=isr(n,k); k=isk(n,k); printf("RESULT: %i\n\n",m); } int isr(int x,int k) int y1=0; int y2=0; int y3=0; y1=0; y2=1; y3=1; if (x==2||(x>2&&k==20)) x=x-1; while (y3<=x) { y1=y1+1; y2=y2+2; y3=y3+y2; return y1; int isk(int n,int k) if (k!=20) { if (k!=n) k=21; else if (k==19) k=0; else k=k+2; } else { k=21; return k; int in() char c=0; int k=0; k=0; putc('N',stdout); putc(':',stdout); putc(9,stdout); c=getc(stdin); if (c=='\n') { printf("INFO: the input must be 1 or 2 digits\n\n"); continue; if (c<'0'||c>'9') { if (c=='\n') break; k=c-'0'; if (c=='\n') { return k; } if (k<2) k=k*10+(c-'0'); else if (k==2&&c=='0') k=20; else { printf("INFO: the input number must be in {0,...,20}\n\n "); if (c!='\n') { 对ISR的要求: 输入为0和20之间的整数时, 输出为其平方根的整数部分。 输入为0和20之间的整数时, 输出为其平方根的整数部分。

测试 黑盒测试 白盒测试 Program testing can be used to show the presence of bugs, but never to show their absence! -- Edsger W. Dijkstra

形式验证 推理验证 模型检测 正确性 正确性+不正确性

例子: ISR 对ISR的要求: (at line 18):((m*m)<=n)&&((m*m)+2*m+1>n) #include <stdio.h> /**************************************************/ int in(); int isr(int x,int k); int isk(int n,int k); int main() { int n=0; int m=0; int k=1; printf("INFO: system is now active\n"); while (1) { n=in(); m=isr(n,k); k=isk(n,k); printf("RESULT: %i\n\n",m); } int isr(int x,int k) int y1=0; int y2=0; int y3=0; y1=0; y2=1; y3=1; if (x==2||(x>2&&k==20)) x=x-1; while (y3<=x) { y1=y1+1; y2=y2+2; y3=y3+y2; return y1; int isk(int n,int k) if (k!=20) { if (k!=n) k=21; else if (k==19) k=0; else k=k+2; } else { k=21; return k; int in() char c=0; int k=0; k=0; putc('N',stdout); putc(':',stdout); putc(9,stdout); c=getc(stdin); if (c=='\n') { printf("INFO: the input must be 1 or 2 digits\n\n"); continue; if (c<'0'||c>'9') { if (c=='\n') break; k=c-'0'; if (c=='\n') { return k; } if (k<2) k=k*10+(c-'0'); else if (k==2&&c=='0') k=20; else { printf("INFO: the input number must be in {0,...,20}\n\n "); if (c!='\n') { 对ISR的要求: (at line 18):((m*m)<=n)&&((m*m)+2*m+1>n)

程序的模型检测(例子)

模型检测 ./verds –c isr.c –sp isr.sp 验证结果 反例

验证过程 Automatic Translator C Program Model VERDS Model Checker Specification Negative Conclusion Error Trace

反例分析 以下输入产生不正确结果 1 3 5 7 9 11 13 15 17 19 0 2 4 6 8 10 12 14 16 18 4 不正确运行

修正后的例子: ISR2 ./isr2 INFO: system is now active N: 2 RESULT: 1 N: 10 #include <stdio.h> /**************************************************/ int in(); int isr(int x,int k); int isk(int n,int k); int main() { int n=0; int m=0; int k=1; printf("INFO: system is now active\n"); while (1) { n=in(); k=isk(n,k); m=isr(n,k); printf("RESULT: %i\n\n",m); } int isr(int x,int k) int y1=0; int y2=0; int y3=0; y1=0; y2=1; y3=1; if (x==2||(x>2&&k==20)) x=x-1; while (y3<=x) { y1=y1+1; y2=y2+2; y3=y3+y2; return y1; int isk(int n,int k) if (k!=20) { if (k!=n) k=21; else if (k==19) k=0; else k=k+2; } else { k=21; return k; int in() char c=0; int k=0; k=0; putc('N',stdout); putc(':',stdout); putc(9,stdout); c=getc(stdin); if (c=='\n') { printf("INFO: the input must be 1 or 2 digits\n\n"); continue; if (c<'0'||c>'9') { if (c=='\n') break; k=c-'0'; if (c=='\n') { return k; } if (k<2) k=k*10+(c-'0'); else if (k==2&&c=='0') k=20; else { printf("INFO: the input number must be in {0,...,20}\n\n "); if (c!='\n') { ./isr2 INFO: system is now active N: 2 RESULT: 1   N: 10 RESULT: 3 N: 20 RESULT: 4 N: 30 INFO: the input number must be in {0,...,20} N: 5 RESULT: 2 N:

模型检测 ./verds –c isr2.c –sp isr.sp 验证结果

验证过程 Automatic Translator C Program Model VERDS Model Checker Specification Positive Conclusion

模型检测的缺点与优点 缺点 可直接验证的程序规模小 可直接验证的程序结构简单 优点: 自动验证 对不正确的程序可生成诊断信息

形式验证 推理验证 模型检测 推理验证与模型检测相结合

推理验证+模型检测 int in() { char c=0; int k=0; while (1) { k=0; … #include <stdio.h> /**************************************************/ int in(); int isr(int x,int k); int isk(int n,int k); int main() { int n=0; int m=0; int k=1; printf("INFO: system is now active\n"); while (1) { n=in(); k=isk(n,k); m=isr(n,k); printf("RESULT: %i\n\n",m); } int isr(int x,int k) int y1=0; int y2=0; int y3=0; y1=0; y2=1; y3=1; if (x==2||(x>2&&k==20)) x=x-1; while (y3<=x) { y1=y1+1; y2=y2+2; y3=y3+y2; return y1; int isk(int n,int k) if (k!=20) { if (k!=n) k=21; else if (k==19) k=0; else k=k+2; } else { k=21; return k; int in() char c=0; int k=0; k=0; putc('N',stdout); putc(':',stdout); putc(9,stdout); c=getc(stdin); if (c=='\n') { printf("INFO: the input must be 1 or 2 digits\n\n"); continue; if (c<'0'||c>'9') { if (c=='\n') break; k=c-'0'; if (c=='\n') { return k; } if (k<2) k=k*10+(c-'0'); else if (k==2&&c=='0') k=20; else { printf("INFO: the input number must be in {0,...,20}\n\n "); if (c!='\n') { int in() { char c=0; int k=0;   while (1) { k=0; … if (c=='\n') { return k; } return k; } k>=0; k<=20; 不可达 k>=0; k<=20;

推理验证+模型检测 int in() FUNCTION r=in() { ASSUMPTION TRUE; char c=0; #include <stdio.h> /**************************************************/ int in(); int isr(int x,int k); int isk(int n,int k); int main() { int n=0; int m=0; int k=1; printf("INFO: system is now active\n"); while (1) { n=in(); k=isk(n,k); m=isr(n,k); printf("RESULT: %i\n\n",m); } int isr(int x,int k) int y1=0; int y2=0; int y3=0; y1=0; y2=1; y3=1; if (x==2||(x>2&&k==20)) x=x-1; while (y3<=x) { y1=y1+1; y2=y2+2; y3=y3+y2; return y1; int isk(int n,int k) if (k!=20) { if (k!=n) k=21; else if (k==19) k=0; else k=k+2; } else { k=21; return k; int in() char c=0; int k=0; k=0; putc('N',stdout); putc(':',stdout); putc(9,stdout); c=getc(stdin); if (c=='\n') { printf("INFO: the input must be 1 or 2 digits\n\n"); continue; if (c<'0'||c>'9') { if (c=='\n') break; k=c-'0'; if (c=='\n') { return k; } if (k<2) k=k*10+(c-'0'); else if (k==2&&c=='0') k=20; else { printf("INFO: the input number must be in {0,...,20}\n\n "); if (c!='\n') { int in() { char c=0; int k=0;   while (1) { k=0; … if (c=='\n') { return k; } return k; } FUNCTION r=in() ASSUMPTION TRUE; GUARANTEE r>=0&&r<=20; k>=0; k<=20; 不可达 k>=0; k<=20;

模型检测 时间优势对比: Time Time (with A/G) Model Checking 1233 205 ./verds –c isr.c –sp isr.sp –fsp isr.fsp 时间优势对比: 验证结果 Time Time (with A/G) Model Checking 1233 205

验证过程 http://lcs.ios.ac.cn/~zwh/verds/ Automatic Translator C Program Model VERDS Model Checker Specification Function Specification Positive Conclusion http://lcs.ios.ac.cn/~zwh/verds/

并发模型的模型检测(例子)

并发模型的模型检测(例子) a=s0 b=t0 x=0 y=0 t=0

并发模型的模型检测 建模 验证问题 Model

并发模型(主程序) VVM VAR x: 0..1; y: 0..1; t: 0..1; INIT x=0; y=0; t=0; PROC p0: p0m(); p1: p1m(); SPEC AG(!(p0.a=s2&p1.b=t2)); AG((!p0.a=s1|AF(p0.a=s2|p1.b=t2))&(!p1.b=t1|AF(p0.a=s2|p1.b=t2))); AG((!p0.a=s1|AF(p0.a=s2))&(!p1.b=t1|AF(p1.b=t2))); AG((!p0.a=s1|EF(p0.a=s2))&(!p1.b=t1|EF(p1.b=t2)));

并发模型(进程模块说明1) MODULE p0m() VAR a: {s0,s1,s2,s3}; INIT a=s0; TRANS a=s0: (y,t,a):=(1,1,s1); a=s1&(x=0|t=0): (a):=(s2); a=s1&!(x=0|t=0): (a):=(s1); a=s2: (y,a):=(0,s3); a=s2: (a):=(s2); a=s3: (y,t,a):=(1,1,s1);

并发模型(进程模块说明2) MODULE p1m() VAR b: {t0,t1,t2,t3}; INIT b=t0; TRANS b=t0: (x,t,b):=(1,0,t1); b=t1&(y=0|t=1): (b):=(t2); b=t1&!(y=0|t=1): (b):=(t1); b=t2: (x,b):=(0,t3); b=t2: (b):=(t2); b=t3: (x,t,b):=(1,0,t1);

模型检测 ./verds -ck 1 me002.vvm VERSION: verds 1.42 - DEC 2012 FILE: me001.vvm PROPERTY: A G ! ((a = 2 )& (b = 2 )) bound = 1 time = 0 ---------- time = 0 bound = 2 time = 0 bound = 3 time = 0 bound = 4 time = 0 bound = 5 time = 0 bound = 6 time = 0 CONCLUSION: TRUE (time=0)

模型检测结论 Property Conclusion AG(!(p0.a=2&p1.a=2)) true AG((!p0.a=1|AF(p0.a=2|p1.a=2))&(!p1.a=1|AF(p0.a=2|p1.a=2))) false AG((!p0.a=1|AF(p0.a=2))&(!p1.a=1|AF(p1.a=2))) AG((!p0.a=1|EF(p0.a=2))&(!p1.a=1|EF(p1.a=2)))

进程公平性说明

并发模型(主程序) VVM VAR x: 0..1; y: 0..1; t: 0..1; INIT x=0; y=0; t=0; PROC p0: p0m(); p1: p1m(); SPEC AG(!(p0.a=s2&p1.b=t2)); AG((!p0.a=s1|AF(p0.a=s2|p1.b=t2))&(!p1.b=t1|AF(p0.a=s2|p1.b=t2))); AG((!p0.a=s1|AF(p0.a=s2))&(!p1.b=t1|AF(p1.b=t2))); AG((!p0.a=s1|EF(p0.a=s2))&(!p1.b=t1|EF(p1.b=t2)));

并发模型(进程模块说明1a) MODULE p0m() VAR a: {s0,s1,s2,s3}; INIT a=s0; TRANS a=s0: (y,t,a):=(1,1,s1); a=s1&(x=0|t=0): (a):=(s2); a=s1&!(x=0|t=0): (a):=(s1); a=s2: (y,a):=(0,s3); a=s2: (a):=(s2); a=s3: (y,t,a):=(1,1,s1); FAIRNESS running;

并发模型(进程模块说明2a) MODULE p1m() VAR b: {t0,t1,t2,t3}; INIT b=t0; TRANS b=t0: (x,t,b):=(1,0,t1); b=t1&(y=0|t=1): (b):=(t2); b=t1&!(y=0|t=1): (b):=(t1); b=t2: (x,b):=(0,t3); b=t2: (b):=(t2); b=t3: (x,t,b):=(1,0,t1); FAIRNESS running;

模型检测结论 Property Conclusion AG(!(p0.a=2&p1.a=2)) true AG((!p0.a=1|AF(p0.a=2|p1.a=2))&(!p1.a=1|AF(p0.a=2|p1.a=2))) AG((!p0.a=1|AF(p0.a=2))&(!p1.a=1|AF(p1.a=2))) false AG((!p0.a=1|EF(p0.a=2))&(!p1.a=1|EF(p1.a=2)))

进程公平性说明2

并发模型(主程序) VVM VAR x: 0..1; y: 0..1; t: 0..1; INIT x=0; y=0; t=0; PROC p0: p0m(); p1: p1m(); SPEC AG(!(p0.a=s2&p1.b=t2)); AG((!p0.a=s1|AF(p0.a=s2|p1.b=t2))&(!p1.b=t1|AF(p0.a=s2|p1.b=t2))); AG((!p0.a=s1|AF(p0.a=s2))&(!p1.b=t1|AF(p1.b=t2))); AG((!p0.a=s1|EF(p0.a=s2))&(!p1.b=t1|EF(p1.b=t2)));

并发模型(进程模块说明1b) MODULE p0m() VAR a: {s0,s1,s2,s3}; INIT a=s0; TRANS a=s0: (y,t,a):=(1,1,s1); a=s1&(x=0|t=0): (a):=(s2); a=s1&!(x=0|t=0): (a):=(s1); a=s2: (y,a):=(0,s3); a=s2: (a):=(s2); a=s3: (y,t,a):=(1,1,s1); FAIRNESS running; a!=s2;

并发模型(进程模块说明2b) MODULE p1m() VAR b: {t0,t1,t2,t3}; INIT b=t0; TRANS b=t0: (x,t,b):=(1,0,t1); b=t1&(y=0|t=1): (b):=(t2); b=t1&!(y=0|t=1): (b):=(t1); b=t2: (x,b):=(0,t3); b=t2: (b):=(t2); b=t3: (x,t,b):=(1,0,t1); FAIRNESS running; b!=t2;

模型检测结论 Property Conclusion AG(!(p0.a=2&p1.a=2)) true AG((!p0.a=1|AF(p0.a=2|p1.a=2))&(!p1.a=1|AF(p0.a=2|p1.a=2))) AG((!p0.a=1|AF(p0.a=2))&(!p1.a=1|AF(p1.a=2))) AG((!p0.a=1|EF(p0.a=2))&(!p1.a=1|EF(p1.a=2)))

验证过程 http://lcs.ios.ac.cn/~zwh/verds/ 建模 验证问题 Model VERDS Model Checker Positive Conclusion Negative Conclusion 安全性质 Error Trace http://lcs.ios.ac.cn/~zwh/verds/

模型检测的学习与研究 学习 应用 研究 原理 相关知识 将其应用于一些简单程序 将其应用于不同类型的模型 建立新方法 改建算法以增加可应用性 与其他方法结合以增加可应用性

模型检测的学习与研究 学习 应用 研究 原理 相关知识 将其应用于一些简单程序 将其应用于不同类型的模型 建立新方法 改建算法以增加可应用性 与其他方法结合以增加可应用性 符号模型检测 限界模型检测 硬件/协议/软件 实时系统模型 概率系统模型 混成系统 抽象方法 反例制导抽象求精 偏序归约 对称技术 组合方法 推理方法

问题?