小编dav*_*der的帖子

大家好，我是一名老 Java/Haskell/Cobol 程序员。Julia 有许多很棒的功能，但我在我认为的基础知识上遇到了困难。特别是如何找到许多包中的内容（通量、绘图、微分方程等）。

1. 我尝试过 VSCode 和 Jupiter Notebook 以及 Julia REPL，但没有找到在编写程序时提取这些重要信息的方法。
2. 我也未能在网上找到信息，而这些信息却很少分布在每个包的教程中。

是否有“cheetsheet”或“summary”或类似java的API？

I am used to loops

while Grd
invariant Inv
{ ..}
assert Inv && !Grd;

没有任何中断，Dafny 知道这Inv && ! Grd 是真的，但是：Dafny 不会检查break;命令后的循环不变式。因此

method tester(s:seq<int>) returns (r:int) 
ensures r <= 0
{   var i:nat := |s|;
    r := 0;
    while (i > 0)
       decreases i
       invariant r == 0;
    {   i := i -1;
        if s[i]< 0  { r:= s[i]; break;}        
    }    
   // assert r == 0; // invariant dose not hold
}

method Main() {
    var x:int …