English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

Refinement types are a popular way to specify and reason about key programproperties. In this paper, we introduce RTR, a new system that adds refinementtypes to Ruby. RTR is built on top of RDL, a Ruby type checker that providesbasic type information for the verification process. RTR works by encoding itsverification problems into Rosette, a solver-aided host language. RTR handlesmixins through assume-guarantee reasoning and uses just-in-time verificationfor metaprogramming. We formalize RTR by showing a translation from a core,Ruby-like language with refinement types into Rosette. We apply RTR to check arange of functional correctness properties on six Ruby programs. We find thatRTR can successfully verify key methods in these programs, taking only a fewminutes to perform verification.

Refinement Types for Ruby