Skip to content

Latest commit

 

History

History
145 lines (104 loc) · 5.2 KB

README.md

File metadata and controls

145 lines (104 loc) · 5.2 KB
Raw

Cassius

Cassius

Cassius is a formalization of CSS, making it possible to build tools that reason about the appearance of web pages.

Installing

To capture web pages (needed to use Cassius) you will need:

Note that Firefox, Geckodriver, and Selenium must have compatible versions.

To run Cassius on the captured web pages, you will need:

Make sure Geckodriver, Typescript, and Z3 are in your path, and Selenium is in your Python path.

First, set up Cassius with:

make setup

Then, test out your Cassius installation by running, from the top-level directory,

python3 capture/capture.py http://example.com/ --output bench/example.rkt
racket src/run.rkt accept bench/example.rkt example.com

This should churn for a few seconds and say, "Accepted".

Capturing Web Pages

To reason about a web page, the page must be captured, converted into Cassius's input format. To capture a web page, run:

python3 capture/capture.py [urls ...] --output [file]

The URLs may be web pages, accessed through the http:// or https:// protocols, or local files, given either by a file:// URL or by a path.

The output file is created or overwritten by this command, and stores one web pages for each given URL. They are named doc-00N, for N from 1 to the number of URLs and the number being zero-padded (these names are referred to as "instances").

Some pages need to be modified before being captured. The --prerun [js-file] flag allows you to run a JavaScript file before capturing the page.

Testing if a Web Page is Supported

To determine whether Cassius supports a given web page, run

racket src/run.rkt accept [file] [instance]

where [instance] is usually doc-1, or maybe doc-2 or similar if you passed several URLs to the capture.py script.

This will churn for a while and output either "Accepted" or "Rejected". If "Accepted" is produced, that means that Cassius's formalization of browser rendering accepts the rendering produced by Firefox, a good proxy for whether Cassius supports your web page.

Cassius currently supports a fragment of CSS 2.1:

  • The CSS 2.1 box model: padding, border, and margins
  • Min and max widths and heights
  • Percentage and em measurements
  • Colors, foreground and background
  • The inline, block, and inline-block display modes
  • line-height and font-size
  • position and the positioning properties
  • float and clear

A few miscellaneous properties, like box-sizing, are also supported.

Testing Assertions with VizAssert

To test some assertions on a web page, write the assertion into a file and run:

racket src/run.rkt assertion [assertion-file] [assertion-name] [file] [instance]

See bench/assertions/assertions.vizassert for an example of the syntax of assertion files. That file contains several assertions drawn from common accessibility and usability guidelines, including:

  • text-size: text should be at least 14px tall
  • contrast: text should have good contrast with background
  • interactive-onscreen: links, buttons, and inputs should be onscreen
  • overlapping-text: text should not overlap other text
  • text-width: text should not be wider than 80 characters
  • line-spacing: line spacing should be at least 1.5
  • paragraph-spacing: paragraph spacing should be at least 1.5 line spacing
  • selected-onscreen: .selected items should be onscreen
  • tab-ordering: tab order should be top down and left to right
  • button-size: buttons should be at least 30×30px
  • link-distinctive: links should be a distinct color from normal text
  • no-horizontal-scroll: no elements should scroll horizontally
  • interactive-distinct: interactive elements should be a different color from non-interactive ones

The chosen assertion will be run on the chosen instance, and if the assertion is false, a counterexample render tree will be printed.

Proving Assertions with VizAssert

VizAssert can also check modular proofs of web pages. Write the proof to a file and run:

racket src/run.rkt check-proof [proof-file]

See bench/fwt.proof for an example of the syntax of proof files. That file contains several proofs of the interactive-onscreen property for various pages, and several proofs of various other properties.

Optional arguments can be added to the above command to name a proof, a page to use that proof for, or even a componentin that page, to check. You can also pass the --threads N argument to check the proof in parallel and the --cache [file] argument to use a proof cache.

Current Status

Cassius development is tracked on Trello. Email Pavel Panchekha to be added to the project.