# Questions tagged [formal-methods]

a particular kind of mathematically-based technique for the specification, development and verification of software and hardware systems.

124 questions
Filter by
Sorted by
Tagged with
32 views

### How to prove that $\lfloor{\sqrt{n}\rfloor} = \Theta(\sqrt{n})$? [duplicate]

It is quite direct to prove that $\lfloor{\sqrt{n}\rfloor} = O(\sqrt{n})$. But how can I prove that $\lfloor{\sqrt{n}\rfloor} = \Omega(\sqrt{n})$?
52 views

### How to prevent the change of other objects in Z specification?

I have Z specification of Banking system, whose fragments are: and I think that the specification is OK, but my professor says that this specifiction is completely wrong, because AddAccount ...
27 views

### Effective method for simulating program's cycle

I'm looking for an effective method to simulate a program. Why I am needing this is because sometimes I can only have the program's description, code, and all I have left is pen and paper when I want ...
438 views

32 views

### Compute Lazily - Model checking

What is meant by lazily computing online? For example, in context of synthesis, that uses model checking. http://www.cs.colostate.edu/~france/CS614/Readings/Readings2011/Model-checking-Survey-a21-...
20 views

### Textbook for Hoare logic

I am looking to understand what Hoare logic is, and how it is used to prove program-correctness. I am interested in an applied text, which shows how to actually state formal specifications of programs,...
23 views

### How to generate tests using Model-Based Testing paradigm (for a newcomer)

So I just learned of Model-Based Testing. It sounds like this is a practical approach to some level of formal verification of production software applications. As I understand it, you have a ...
17 views

### Does formal specification of UX needs special language apart from the general specification languages?

I am fan of Alloy and CASL specification languages and my question is - what is the common practice regarding the formal methods in UX? Does UX require distinct specification languages? Generally one ...
20 views

### How to solve Hoare's problem when precondition contains meta symbols?

This is the proram for which I have to prove correctness using Hoare's Axioms: {X = |x|} if(x<=0) x:=-x; else skip; {X=x} This is my solution so ...
35 views

### Confusion regarding algebraic specification of the queue

I was given the following question in the test where I had to write the algebraic specification and its axioms based on below-defined operations: ...
15 views

### State-machine semantics of instruction set architectures

An instruction set architecture is an abstraction, a common interface layer between the software and the micro-architecture. The existence of this clearly delineated interface is becoming increasingly ...
33 views

### Formal language representation of program

I have numerous records, composed of words. Each word gets translated into vectors, with a variable number of channels, provided that that word exists in a specific lookup dictionary. For n number of ...
17 views

### What is the name for the theory that guarantees proof for negative and not for all possible positives

I have heard of some people mentioning the general rule that says that you can only ever guarantee that a program will not capture the negative cases but you can never guarantee that it captures all ...