Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

  • Andrei Paskevich's avatar
    WhyML: white-box blocks · 516cfd3a
    Andrei Paskevich authored
    Just as abstract blocks, "white-box blocks" are program expressions
    with an additional contract attached to their execution place.
    Contrary to abstract blocks, whiteboxes do not hide their contents
    from the outer computation. In most cases, you would not need
    whiteboxes at all, as the same effect can be achieved by adding
    assertions. Their utility comes from their syntax: the added
    contract clauses bind to the expression and do not require
    additional semicolons, begin-end's, let-in's or try-with's.
    
    Compare:
    
        let x = <expr> in assert { P x }; x
    to  <expr> ensures { P result }
    or  <expr> returns { x -> P x }
    
        if ... then begin let x = <expr> in assert { P x }; x end; ...
    to  if ... then <expr> ensures { P result }; ...
    
        try <expr> with E x -> assert { P x }; raise E x; end
    to  <expr> raises { E x -> P x }
    
    Internally, whiteboxes are just abstract blocks (zero-argument
    anonymous functions executed in-place) with the label "vc:white_box"
    on top. The user never needs to write this label explicitly though.
    516cfd3a
vc.mli 1.03 KB