Skip to content

kochetov-dmitrij/WeakestPrecondition

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

40 Commits
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

What is this

The aim of the project is to visualize the process of the weakest precondition's computing

Where is it working

What was used

  • There is being used React framework, JavaScript

Work process

  • You enter a program in TEL programming language and a postcondition for the program, after that press button, and you will see first step of computing of the weakest precondition using special notation, to proceed process of computing choose appropriate block of 'wp[Index]' and click that, you will see next step, when a precondition computing for a block is completed, there is a button '=Substitute all wp[Index]=', when it is pressed, you can see how all occurrences of current block will be replaced with computed precondition for the 'wp[Index]' block.

Final report

TEL programming language

  • Description

    TEL is a fictional programminng language designed for educational purposes.

  • Notation

    BNF:
    • <const_or_var> ::= <constant> | <variable>
    • <relation> ::= = | > | < | ~= | >= | <=
    • <operation> ::= | + | -
    • <expression> ::= <const_or_var> |
              <const_or_var> <bln> <operation> <bln> <const_or_var>
    • <assignment> ::= <variable> <bln> := <bln> <expression>
    • <comparison> ::= <const_or_var> <bln> <relation> <bln> <const_or_var>
    • <program> ::= <assignment> |
              <bln> <program> <bln> |
              (<bln> <program> <n/s> ; <n/s> <program> <n/s>) |
              (<bln> IF <n/s> <spc> <comparison> <spc> <n/s> THEN <n/s> <program> <n/s> ELSE <n/s> <program> <n/s> ) |
              (<bln> WHILE <n/s><spc> <comparison> <spc><n/s> DO <n/s> <program> <n/s> ) |         (<bln> WIN <n/s> <spc> <formula> <spc> <n/s> EOI <n/s> <spc> <comparison> <spc> <n/s> DO <n/s> <program> <n/s> )
    Comment on notation:
    • All concepts are in angles “< >”.
    • All terminal symbols (but spacing symbols) are as they depicted.
    • All explicit spacing in the definition above is just for structuring and readability.
    • <spc> stays for the single blank space.
    • <bln> stays for any (including zero) number of <spc>.
    • <n/s> stays for a single new line or a single blank space.
    • <constant> stays for any integer in decimal notation (leading zeros are admissible).
    • <variable> stays for any sequence of low-case Latin letters and decimal digits staring with aletter.
    • <formula> stays for any sequence of low-case Latin letters, decimal digits, <operation> and
    • <relation> symbols, and parenthesis ‘(‘ and ‘)’ balanced with respect to parenthesis, i.e.
    • The total number of ‘(‘ is equal to the total number of ‘)’,
    • Scanning from left to right the number ‘(‘ is never less than the number of ‘)’.
  • TEL program example

    • program32 := start ;
      (IF  q = x  THEN
          z := 0 ;
          fo := m2 + 13
      ELSE
          pre := condition ;
          formal := semantics ;
          (IF  max =d  THEN d :=0- max ELSE s33 := var ) ;
          dmitry := kochetov ;
          maxim := popov ;
          (WIN  x < u  EOI  x = y  DO
              qwe := 13
          )
      )

    • If you get a parse exception it's most likely you type one space char instead of 2 space chars which is specified in BNF

  • Postcondition example

    • x >= formal
    • !(x<formal) && (dmitry + (pre * formal)) < 13
    • (x>formal || r12 ~= 22) && (dmitry - 1) < 13 || q > e

Screenshots

About

Visualised process of the weakest precondition's computing

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published