首页 > 编程语言 >Floyd归纳断言法验证程序部分正确性

Floyd归纳断言法验证程序部分正确性

时间:2023-12-05 19:57:00浏览次数:37  
标签:通路 断言 Floyd 程序 正确性 写为 例题

1.设断点

  一般我们会在如下位置设置断点:

  (1)程序开始处

  (2)程序结束处

  (3)循环主干处

2.建断言

  (1)开始处A:

    一般为题干的要求,写为

 

  (2)结束处C:

    一般为输出结果z,写为

 

  (3)循环主干处:

    (写为

    此处断言最为难建立,一般有三种方法得出断言:

      1)从结果倒推

      2)观察题目及规约条件

      3)靠灵感

3.设通路检验条件

  此处为我比较主观的写法,可能会有些看不懂

  

 

4.证明通路检验条件

  (1)等用断言替换

  (2)"->"后部分的式子写为变化后的式子,以下有一个例子

    将各通路全证为真后则可以证明该程序的部分正确性。

5.例题

  以下是一个例题,上面还有我们老师的提示(不过本例题的断言不采用老师的提示版本)

  

   以下为证明过程(因为之前是写给自己看的所以会有很多我自己能看懂可能大家看不懂的东西,之后会一一加上解释(大概)):

         

 


 

*如有问题欢迎指出!  

标签:通路,断言,Floyd,程序,正确性,写为,例题
From: https://www.cnblogs.com/lavendery/p/17877967.html

相关文章

  • 4、类型断言
    类型断言(TypeAssertion)可以用来手动指定一个值的类型。类型断言constbox=document.querySelector('.box')//<类型>数据console.log((<HTMLDivElement>box).innerHTML)//值as类型console.log((boxasHTMLDivElement).innerHTML)在tsx语法(React的jsx语法的......
  • 第 132 场周赛——质数小结论,并查集配Floyd
    https://www.acwing.com/activity/content/competition/problem_list/3648/B题收获:1.利用题目告诉的结论:1e9范围质数之差小于3002.一个数不被2-a的任何数整除等价于他的最小质因子需要大于ac题:初步宏观思路:不难想到用并查集维护类别,只需将每一个类缩成一个点,由于最多只有500......
  • JMeter基础 — JMeter中BeanShell断言详解
    JMeter中的BeanShell断言,可以使用BeanShell脚本来执行断言检查,可以用于更复杂的个性化需求,使用更灵活,功能更强大,但是要能够熟练使用BeanShell语。1、BeanShell简介Beanshell是一种类似JAVA的脚本语言,通过BeanShell可以对请求数据、响应数据或环境变量进行更加灵活的处理和判断。......
  • 关键字 开发-09 validate断言
    1.yaml文件中添加validate进行接口断言首先我们在utils/validate.py文件添加需要的断言方式importredefequals(check_value,expect_value):assertcheck_value==expect_value,f'{check_value}=={expect_value}'defless_than(check_value,expect_value):......
  • Jmeter接口自动化测试 —— Jmeter断言之Json断言
     json断言可以让我们很快的定位到响应数据中的某一字段,当然前提是响应数据是json格式的,所以如果响应数据为json格式的话,使用json断言还是相当方便的。还是以之前的接口举例Url:https://data.cma.cn/weatherGis/web/weather/weatherFcst/getCurrentConditionHTTPMethod:Po......
  • jmeter断言
     断言是在请求的返回层面增加一层判断机制。因为请求成功了,并不代表结果一定正确,因此需要检测机制提高测试准确性。现在介绍三种常用断言。 1.响应断言在取样器上添加响应断言,如下图:  添加响应断言后,再添加一个“断言结果”。 ......
  • SpringCloud——自定义断言工厂
    目录场景:用户的请求头中需要有指定的用户名和密码才能访问。断言工厂参考系统AfterRoutePredicateFactory写法。packagecom.zjw.factory;importlombok.Getter;importlombok.Setter;importorg.springframework.cloud.gateway.handler.predicate.AbstractRoutePredi......
  • floyd算法
    FLOYD复杂度Floyd-Warshall算法的时间复杂度为O(|V|^{3})[4],空间复杂度为O(|V|^{2}),其中V是点集。原理动态规划适用范围Floyd-Warshall算法适用于解决带权有向图或带权无向图的全源最短路径问题,即计算任意两个顶点之间的最短路径长度。Floyd-Warshall算法的适用范围包......
  • 微服务 Gateway 网关——路由断言工厂
    路由断言工厂RoutePredicateFactory我们在配置文件中写的断言规则只是字符串,这些字符串会被 PredicateFactory读取并处理,转变为路由判断的条件  ......
  • jmeter中断言失败后不继续执行后续的取样器,以及失败事务个数的统计
    需要实现的场景:N款产品自动投保,需要统计成功投保的有多少款,失败投保的有多少款?遇到的问题处理:问题一、某款产品投保时,若其中一个接口断言失败,如何让后续接口不继续执行?答:通过if控制器进行处理,  问题二:如何解决统计失败或成功执行的产品数?答:通过事务处理器+BeanShell......