微软搞的达芙妮,很弱呀

版主: hci

回复
头像
(ヅ)楼主
著名点评
著名点评
帖子: 4568
注册时间: 8月 21, 2022, 2:20 pm

微软搞的达芙妮,很弱呀

帖子 (ヅ)楼主 »

连这么简单的代码都没法确认,而且行为诡异

代码: 全选

method Test(){
    var S := set s: int | 0 <= s < 4 :: s * 2; // S == {
    assert 4 in S; // fail
}
加上一行assert还是fail

代码: 全选

method Test(){
    var S := set s: int | 0 <= s < 4 :: s * 2;
    assert S <= {0,2,4,6}; // pass
    assert 4 in S; // fail
}
但是如果加上另一行,这个assert 4 in S就pass了,同时加这一行还会fail

代码: 全选

method Test(){
    var S := set s: int | 0 <= s < 4 :: s * 2;
    assert S <= {0,2,4,6}; // pass
    assert S == {0,2,4,6}; // faill
    assert 4 in S; // WILL PASS
}
简直就是一个巨大的dafuq
图片
whitepaper
著名点评
著名点评
帖子: 4547
注册时间: 7月 23, 2022, 1:07 am
来自: 平凡的地方

Re: 微软搞的达芙妮,很弱呀

帖子 whitepaper »

看不懂这是在干嘛,太高深了
头像
(ヅ)楼主
著名点评
著名点评
帖子: 4568
注册时间: 8月 21, 2022, 2:20 pm

Re: 微软搞的达芙妮,很弱呀

帖子 (ヅ)楼主 »

whitepaper 写了: 12月 1, 2022, 1:54 pm 看不懂这是在干嘛,太高深了
不高深,就是你码字的时候自动实现部分的逻辑验证,能找corner cases,自动防止越界什么的。一边写逻辑,一边就能test

https://github.com/dafny-lang/dafny

上面第一个例子就是断言4\in {0,2,4,6},甚至更简单的,连集合S大小都没办法算出来,没有S.size()这个方法或者属性.

现实很骨感
图片
回复

回到 “葵花宝典(Programming)”