程序代写 Week 6: Model Validation

Week 6: Model Validation
Dr Steffen Zschaler

Goals for today

Today we will look at how to validate models
– How can we support users in producing models that are meaningful and error free? – How does working with a DSML help us give better validation feedback to users?
– How do we build different kinds of validators for our DSMLs?
21/02/2020 (c) King’s College London 2

Fundamentals of validation

What’s the most important thing about code?
What is the primary purpose of code?
– Machine execution
– Human communication and problem solving
21/02/2020 (c) King’s College London 4

What’s the most important thing about code?
What is the primary purpose of code?
– Machine execution
– Human communication and problem solving
What do we need to support this?
– Syntax that is understandable by (the right) humans – Support for problem solving
21/02/2020 (c) King’s College London 4

What’s the most important thing about code?
What is the primary purpose of code?
– Machine execution
– Human communication and problem solving
What do we need to support this?
– Support for problem solving
We have this.
Syntax that is understandable by (the right) humans
21/02/2020 (c) King’s College London

What’s the most important thing about code?
What is the primary purpose of code?
– Machine execution
– Human communication and problem solving
What do we need to support this?
– Syntax that is understandable by (the right) humans –
But what about this?
Support for problem solving
21/02/2020 (c) King’s College London

Problem-solving support: Validation
Goal: Help us better understand what we’re modelling
– We’re building software for complex problems
– Cannot oversee every implication of every decision
– Tools that point out (potential) problems would be helpful
– Called validation
– So would tools that show (partial) results etc.
– Won’t build today, but similar ideas apply
– E.g., check out “code minings” in Eclipse (these are supported by Xtext)
21/02/2020 (c) King’s College London 5

How do DSMLs help in validation?
Consider the Minesweeper implementation
– Cells can be in different states: hidden, discovered, flagged, …
– Implementation of how the state of a cell changes is all over the place in the code – Can we find out, whether all states can actually be reached?
Consider the two different implementations: Java / GridGames DSML
– What would a validation tool need to look at in each case to find cell states that aren’t reachable?
– Discuss with your neighbour and come up with a plan for each case – We’ll then discuss in the whole class and summarise
– Prepare a response – You have 5 minutes
21/02/2020 (c) King’s College London 6

How do DSMLs help in validation?
What would a validation tool need to look at in each case to find cell states that aren’t reachable? Java-based implementation DSML implementation
21/02/2020 (c) King’s College London

How do DSMLs help in validation?
What would a validation tool need to look at in each case to find cell states that aren’t reachable?
Java-based implementation
1. Identify which part of the Java code represents cell states
– This is brittle: needs to make assumptions about the code being written in a regular form
– Humans don’t do that
2. Identify which states belong to the same cell type
3. Identify where and how transitions are encoded
– There are many different ways for doing this
4. Build a reachability graph and analyse it
5. Identify the correct place in the code to annotate
– Brittle again
DSML implementation
1. Identify cell, cell states, and transitions
– Easy and robust: they’re there explicitly
21/02/2020 (c) King’s College London
2. Build a reachability graph and analyse it 3. Identify where to annotate
– Easy and robust: just annotate the unreachable states

How do DSMLs help in validation?
What would a validation tool need to look at in each case to find cell states that aren’t reachable?
Java-based implementation
1. Identify which part of the Java code represents cell states
– This is brittle: needs to make assumptions about the code being written in a regular form
– Humans don’t do that
2. Identify which states belong to the same cell type
3. Identify where and how transitions are encoded
– There are many different ways for doing this
4. Build a reachability graph and analyse it
5. Identify the correct place in the code to annotate
– Brittle again
Overall: no guarantees that the analysis will be
correct and robust
DSML implementation
1. Identify cell, cell states, and transitions
– Easy and robust: they’re there explicitly
21/02/2020 (c) King’s College London
2. Build a reachability graph and analyse it 3. Identify where to annotate
– Easy and robust: just annotate the unreachable states
Overall: information is directly available at the right abstraction. This enables robust analysis.

How do DSMLs help in validation?
What would a validation tool need to look at in each case to find cell states that aren’t reachable?
Java-based implementation
1. Identify which part of the Java code represents cell states
– This is brittle: needs to make assumptions about the code being written in a regular form
– Humans don’t do that
2. Identify which states belong to the same ce
DSML implementation
1. Identify cell, cell states, and transitions
– Easy and robust: they’re there explicitly
3. Identify where and how transitions are encoded – There are many different ways for doing this
4. Build a reachability graph and analyse it
5. Identify the correct place in the code to annotate
– Brittle again
Overall: no guarantees that the analysis will be
correct and robust
2. Build a reachability graph and analyse it 3. Identify where to annotate
– Easy and robust: just annotate the unreachable states
Overall: information is directly available at the right abstraction. This enables robust analysis.
21/02/2020 (c) King’s College London
raction is the key to better validation

Gridgame validation of unreachable states
21/02/2020 (c) King’s College London 9

Implementation of validation
DSML validation happens directly on the abstract syntax
– In an EMF world, can use many different tools for this, regardless of how language was built – Xtend / Java code integrated with EMF validation through Xtext
– Specialist languages, e.g.:
– Epsilon Validation Language (EVL) – XSemantics
– Other language workbenches have their own validation frameworks, e.g.: – Validation rules in Sirius (though can use other EMF validations, too) – Check rules in MPS (see later)
21/02/2020 (c) King’s College London 10

What checks are possible?
Anything can be checked
– But beware the cost
– Usually, limit to static analysis→without “executing” the model
21/02/2020 (c) King’s College London 11

What checks are possible?
Anything can be checked
– But beware the cost
– Usually, limit to static analysis→without “executing” the model
– Local checks
– Check an individual model element’s properties
– May query other model elements starting from the one to be checked – E.g., style checks for names, value ranges, …
– Global checks
– Check an entire model
– E.g., check state reachability
– Control flow analysis, data flow analysis, type checking, …
21/02/2020 (c) King’s College London 11

What checks are possible?
Anything can be checked
– But beware the cost
– Usually, limit to static analysis→without “executing” the model
– Local checks
– Check an individual model element’s properties
– May query other model elements starting from the one to be checked We will look at a simple check, a simple
– E.g., style checks for names, value ranges, …
– Global checks
– Check an entire model
– E.g., check state reachability
– Control flow analysis, data flow analysis, type checking, …
(simplistic) data flow analysis, and at
type analysis.
21/02/2020 (c) King’s College London 11

Building checks in Xtend

Building checks in generates a validator for your language
– A class in the validation package
– Checks are defined as methods in this class,
annotated with @Check
21/02/2020 (c) King’s College London 13

Building checks in generates a validator for your language
– A class in the validation package
– Checks are defined as methods in this class,
annotated with @Check
Uses explicit calls to error / warning methods to create error and warning messages
21/02/2020 (c) King’s College London 13

Building checks in generates a validator for your language
– A class in the validation package
– Checks are defined as methods in this class,
annotated with @Check
Ecore feature that points to the wrong thing – use MyDSLPackage.Literals.XXX constants to find this feature.
Here, we are going to mark the name of a greeting.
21/02/2020 (c) King’s College London 13

Building checks in generates a validator for your language
– A class in the validation package
– Checks are defined as methods in this class,
annotated with @Check
A string constant identifying the type of error for easy internal reference. Must uniquely identify the error type.
21/02/2020 (c) King’s College London 13

Building checks in generates a validator for your language
– A class in the validation package
– Checks are defined as methods in this class,
annotated with @Check
– Object to which to attach the message is
automatically identified
– If needed, can also be explicitly given
21/02/2020 (c) King’s College London 13

In your pairs
– Extend your turtles implementation with a validation that warns when variable names don’t start with a lower-case letter
– Test your check in the editor
– Bonus points if you can work out how to extend your Xpect tests to test your checker You have 15 minutes
Download last step as tag DSML_v13_pre_validation from the Turtles repository linked from KEATS
(Note: you may need to use the new link for this week)
21/02/2020 (c) King’s College London 14

Ensuring correctness: grammar vs validator
Where is the best place to ensure structural rules?
– Could have enforced naming rule in the grammar – Why didn’t we?
– Better error messages
– “Variable names should start with a lower-case letter” vs “couldn’t parse TheVariable”
– Better error recovery
– Parse errors can very quickly mean nothing beyond the error is processed
– Thus, can hide more serious problems and make them difficult to spot and fix – Can provide quick fixes via validator, but not via parser
– It’s generally better to defer validation and only enforce the minimum necessary in the grammar and abstract syntax
21/02/2020 (c) King’s College London 17

More complex checks

Control-flow graphs
DSML checks can be anything
But it’s worth knowing about some established techniques – e.g., control-flow graphs (CFGs)
– Graphs representing the structure of program
– What instructions happen before/after what others
– Components
– Basic blocks: linear sequence of instructions – Edges for possible jumps
– Overapproximate set of possible paths
– Can be used for a number of static analyses
– For example dead-code analysis, returns on all paths, …
– Underpins data-flow analysis (which also looks at what the steps do)
21/02/2020 (c) King’s College London 19

Data-flow analysis
Basic idea: traverse the CFG and update tracker with information at each stage
– Approximation of what would really happen: we’re trying to analyse without running the program – Determine range of possible values for a variable
– Determine if a variable is not null – Null, NotNull, Maybe
– Can be described with type-checking rules (see later) – But for simple cases easier to program out
– Pattern:
– Initialise knowledge base (a data structure with our knowledge of the analysis outcome) – Traverse the CFG (for iterative languages, may simply traverse the program)
– E.g., using Xtend fold over statement lists
– Use dispatch method to update knowledge base for each step
– For loops and branches, recursively traverse the contained steps – Interpret resulting knowledge base
21/02/2020 (c) King’s College London 20

An example analysis for Turtle programs
Turtles draw lines
– For these, they use a pen
– New commands: pen up / pen down
– A program with the pen up at the end, may not actually have drawn a line
– We can use data-flow analysis to determine if the pen is down at the end of the program
– Remember our pattern:
– Initialise knowledge base: a Boolean value set to true to indicate that the pen is initially down – Traverse the CFG / the Turtle program
– Using Xtend fold over the list of statements
– Use dispatch method to update knowledge base for each step
21/02/2020 (c) King’s College London 21

Pragmatics: diff

程序代写 CS代考加微信: powcoder QQ: 1823890830 Email: powcoder@163.com

Related Posts