The Coq source code can be downloaded here.
The file fletch_main.v
contains the message safety theorem and proof.
The implementation of message-safe and strict type checkers can be downloaded here.
In order to be able to run our experiments, please follow the steps below:
unzip DartSources.zip
gclient
is on your path environment variablegclient sync --revision 45011 -n && gclient runhooks
./main.sh compile
, otherwise follow
the instructions here(pathToFolder)/dartRep/dart-repo/dart/out/ReleaseX64/dart-sdk/bin
where (pathToFolder)
is the path to the
DartSources
directory and ReleaseX64/
might change depending on your operating system version./main.sh
to run the experiments (see README.txt
for more details about the experiments)pub cache repair
When you run the experiments typing ./main.sh
, a graphical interface will appear, and after the experiment execution a pdf file
will be generated and displayed.
If you have trouble running the experiments, or some tool such as latex is not installed on your machine, you can type
./benchmarks.sh (name)
, where (name)
is the benchmark name (for example dart2js).
This command will prompt the experiment result as plain text.
If you set the environment variable as mentioned above, you can run the type checker on a single file file.dart
with the standard Dart
type checker by typing dartanalyzer file.dart
.
If you want to use the message-safety type checker you can run dartanalyzer --message-safe file.dart
,
and to run the full type safety checker type dartanalyzer --message-safe --strict file.dart